diff --git a/buildjob b/buildjob
index b5897aaf1732bedc650b75d05b753db6214a524b..2ab2088f1895487d0f84b66000a6f9a6916bcd4c 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"