diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cc80845e81..09ed198547 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -303,7 +303,7 @@ hadrian-ghc-in-ghci: git config user.name "GHC GitLab CI" - | THREADS=`mk/detect-cpu-count.sh` - make $TEST_TYPE THREADS=$THREADS JUNIT_FILE=../../junit.xml METRICS_FILE=$METRICS_FILE + make $TEST_TYPE THREADS=$THREADS JUNIT_FILE=../../junit.xml METRICS_FILE=$METRICS_FILE || (METRICS_FILE=$METRICS_FILE .gitlab/push-test-metrics.sh && false) - | # Push git notes. METRICS_FILE=$METRICS_FILE .gitlab/push-test-metrics.sh |