diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-13 05:15:26 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-13 05:15:26 -0500 |
| commit | b6bbd58e562b7267e0809f4eff4043ec86285003 (patch) | |
| tree | fdc850187d5ffcbee650008fbf30e6226f7a3877 /etc | |
| parent | 72926462e4f24d558c6ecc7c0ad773427905b3d1 (diff) | |
Also build non-specific on smithers
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/ci/smithers.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh index 247ab0690..643a66764 100755 --- a/etc/ci/smithers.sh +++ b/etc/ci/smithers.sh @@ -8,7 +8,7 @@ export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH" coqtop -v echo | coqtop export TARGETS="coq display bench test" -export TARGETS="coq nonautogenerated-specific nonautogenerated-specific-display" # bench test" # bench and test don't work on smithers +export TARGETS="coq non-specific nonautogenerated-specific nonautogenerated-specific-display" # bench test" # bench and test don't work on smithers 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 |