From 1debe206dff53dfb20795ddf40d0a328d2252a6f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 31 Dec 2020 18:22:08 -0500
Subject: [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.
---
 dev/ci/ci-coq_performance_tests.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'dev')

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 )
-- 
cgit v1.2.3