no time by default

3f472699 · Michael Sammler · d948c3b2 · 3f472699
Commit 3f472699 authored Nov 26, 2020 by Michael Sammler
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

build.sh build.sh +1 -1

No files found.
--- a/build.sh
+++ b/build.sh
@@ -2,7 +2,7 @@

 set -e

-export TIMECMD="time -f \t%es\t%P"
+# export TIMECMD="time -f \t%es\t%P"

 if [[ "${1##*.}" == "c" ]]; then
    dune exec -- refinedc check --no-build "$1"