diff options
author | Zubin Duggal <zubin.duggal@gmail.com> | 2022-01-18 18:55:40 +0530 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-01-18 20:47:23 -0500 |
commit | 85dc61ee14049c85ab342747b0c2669e5ba3f55f (patch) | |
tree | 54c5c5c5d67ae0ad4dfcacc6a76db270f53f2298 /.gitlab/ci.sh | |
parent | fd0019a0381b4c76557063e97ff462acd617e4c2 (diff) | |
download | haskell-85dc61ee14049c85ab342747b0c2669e5ba3f55f.tar.gz |
ci: Fix subtlety with not taking effect because of time_it (#20898)
Diffstat (limited to '.gitlab/ci.sh')
-rwxr-xr-x | .gitlab/ci.sh | 5 |
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) |