From 99c935d2007358fe4028560e96f9c136e608e696 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 9 May 2018 18:26:29 +0200
Subject: [PATCH] allow opting out of the axiom check
---
buildjob | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/buildjob b/buildjob
index b5897aa..2ab2088 100755
--- a/buildjob
+++ b/buildjob
@@ -34,10 +34,17 @@ fi
# Build
echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
time make --output-sync --no-print-directory -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt
-if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi
echo_color "$BOLDGREEN" "[buildjob] Build time summary"
cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt
+# maybe check for axioms
+if [[ -z "$AXIOMS_IGNORE" ]]; then
+ if fgrep Axiom build-log.txt >/dev/null; then
+ echo_color "$BOLDRED" "You used axioms, shame on you!"
+ exit 1
+ fi
+fi
+
# maybe submit timing information
if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
--
GitLab