Commit 99c935d2 authored by Ralf Jung's avatar Ralf Jung

allow opting out of the axiom check

parent 40b71102
......@@ -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"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment