From 9a1d53864a9006ed2e8b64c56db51bdbccdff25a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 25 Nov 2020 08:25:20 +0100
Subject: [PATCH] added build.sh

---
 build.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100755 build.sh

diff --git a/build.sh b/build.sh
new file mode 100755
index 0000000..4ca9a1e
--- /dev/null
+++ b/build.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+export TIMECMD="time -f \t%es\t%P"
+
+if [[ "${1##*.}" == "c" ]]; then
+    dune exec -- refinedc check --no-build "$1"
+    cd "$(dirname $1)/proofs/$(basename $1 .c)"
+    dune build --display short
+else
+    dune build --display short "$@"
+fi
-- 
GitLab