diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-13 17:19:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-13 17:19:12 -0400 |
| commit | 1ad6f6ba1e91d021f207b2fbdcabfbd537633903 (patch) | |
| tree | 5499972000dbe4929ac317638ac8eb81244f1db7 /etc | |
| parent | 0194bc4a99e57fdded7d6132debed20e5e19ce32 (diff) | |
Update smithers script
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/ci/smithers.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh index 0d0cce75a..3532cc3bc 100755 --- a/etc/ci/smithers.sh +++ b/etc/ci/smithers.sh @@ -10,4 +10,5 @@ rm -f BUILD.ok ((/opt/timeout/default-timeout make -j$(nproc) TIMED=1 PROFILE=1 $TARGETS || make STDTIME='/opt/timeout/time-default-timeout-coq -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 PROFILE=1 $TARGETS) && touch BUILD.ok) 2>&1 | tee time-of-build.log python ./etc/coq-scripts/timing/make-one-time-file.py time-of-build.log time-of-build-pretty.log cat time-of-build-pretty.log +/opt/timeout/default-timeout make -j$(nproc) TIMED=1 PROFILE=1 $TARGETS || make STDTIME='/opt/timeout/time-default-timeout-coq -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 PROFILE=1 $TARGETS rm BUILD.ok |