summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorZubin Duggal <zubin.duggal@gmail.com>2022-01-18 18:55:40 +0530
committerMarge Bot <ben+marge-bot@smart-cactus.org>2022-01-18 20:47:23 -0500
commit85dc61ee14049c85ab342747b0c2669e5ba3f55f (patch)
tree54c5c5c5d67ae0ad4dfcacc6a76db270f53f2298
parentfd0019a0381b4c76557063e97ff462acd617e4c2 (diff)
downloadhaskell-85dc61ee14049c85ab342747b0c2669e5ba3f55f.tar.gz
ci: Fix subtlety with not taking effect because of time_it (#20898)
-rwxr-xr-x.gitlab/ci.sh5
1 files changed, 4 insertions, 1 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh
index 776eff3a4a..c30f5ec846 100755
--- a/.gitlab/ci.sh
+++ b/.gitlab/ci.sh
@@ -25,7 +25,10 @@ function time_it() {
shift
local start=$(date +%s)
local res=0
- $@ || res=$?
+ set +e
+ ( set -e ; $@ )
+ res=$?
+ set -e
local end=$(date +%s)
local delta=$(expr $end - $start)