diff options
| author | Jason Gross | 2020-12-31 18:22:08 -0500 |
|---|---|---|
| committer | Jason Gross | 2021-01-11 22:18:44 -0500 |
| commit | 1debe206dff53dfb20795ddf40d0a328d2252a6f (patch) | |
| tree | ee3e3332f2726c3fe4bb5c2be3344d96b423ab56 /dev | |
| parent | 039f04c2caf7c8da380ca8d582e9edae3e6d5c06 (diff) | |
[ci] [coq-performance-tests] Errors at end of log
By running `make -k; make` whenever `make` initially fails, we can get
error messages to occur at the end of the log. This way they'll show up
on the GitHub Actions preview/summary, rather than me having to go
digging for them in the GitLab logs.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-coq_performance_tests.sh | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh index fde8df8e3d..2fa4d5c776 100755 --- a/dev/ci/ci-coq_performance_tests.sh +++ b/dev/ci/ci-coq_performance_tests.sh @@ -5,4 +5,9 @@ ci_dir="$(dirname "$0")" git_download coq_performance_tests -( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf-Sanity && make validate && make install ) +# run make -k; make again if make fails so that the failing file comes last, so that it's easier to find the error messages in the CI log +function make_full() { + if ! make -k "$@"; then make -k "$@"; exit 1; fi +} + +( cd "${CI_BUILD_DIR}/coq_performance_tests" && make_full coq perf-Sanity && make validate && make install ) |