From d19f4835c5ae4fc8d8a324a27f5455451f3a1896 Mon Sep 17 00:00:00 2001
From: Jakob Odersky <jakob@odersky.com>
Date: Sat, 5 Jan 2019 22:03:40 +0100
Subject: Initial commit

---
 .ci/run | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100755 .ci/run

diff --git a/.ci/run b/.ci/run
new file mode 100755
index 0000000..0dbab35
--- /dev/null
+++ b/.ci/run
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+echo "Hello, world!"
+sleep 1
+echo "Done" >&2
+exit 0
\ No newline at end of file
-- 
cgit v1.2.3