diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-11 01:36:21 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-11 01:36:21 -0400 |
| commit | 7aeff23392936b21b8dc590b2cf1823cce180dc5 (patch) | |
| tree | 723e033daae6a9c908b98f2b79e8d6b52676adbc /etc | |
| parent | aa81e1ffd569bde9012164b27b0fd01190f6aa0b (diff) | |
Smithers doesn't support -o pipefail
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/ci/smithers.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh index 9109251b2..0d0cce75a 100755 --- a/etc/ci/smithers.sh +++ b/etc/ci/smithers.sh @@ -1,11 +1,13 @@ #!/usr/bin/bash -set -exo pipefail +set -ex cd "$WORKSPACE" export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH" . /opt/bashrc/bashrc export TARGETS="coq display bench test" -(/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) 2>&1 | tee time-of-build.log +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 +rm BUILD.ok |