diff options
| author | coqbot-app[bot] | 2021-01-12 08:41:18 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-12 08:41:18 +0000 |
| commit | bedea3079b35982abefe4b78ae7aa0f6819842f6 (patch) | |
| tree | dfa95db55923ffb2d7175ac18a0aa2e6bc2b7250 /dev/ci | |
| parent | 89a44a12abc11d867d865494c28e47fe1a0a4d5b (diff) | |
| parent | 1debe206dff53dfb20795ddf40d0a328d2252a6f (diff) | |
Merge PR #13704: [ci] [coq-performance-tests] Errors at end of log
Reviewed-by: SkySkimmer
Ack-by: gares
Diffstat (limited to 'dev/ci')
| -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 ) |