diff options
| -rwxr-xr-x | .gitlab/ci.sh | 9 | ||||
| -rw-r--r-- | .gitlab/common.sh | 4 |
2 files changed, 9 insertions, 4 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index a647698303..962cc7063f 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -18,6 +18,7 @@ fi CABAL_CACHE="$TOP/${CABAL_CACHE:-cabal-cache}" +# shellcheck source=.gitlab/common.sh source "$TOP/.gitlab/common.sh" function time_it() { @@ -597,11 +598,11 @@ function run_hadrian() { # A convenience function to allow debugging in the CI environment. function shell() { - local cmd="*@" - if [ -z "$cmd" ]; then - cmd="bash -i" + local cmd=( "$@" ) + if [ -z "${cmd[*]}" ]; then + cmd=( "bash" "-i" ) fi - run "$cmd" + run "${cmd[@]}" } setup_locale diff --git a/.gitlab/common.sh b/.gitlab/common.sh index befb1493eb..6c487b9911 100644 --- a/.gitlab/common.sh +++ b/.gitlab/common.sh @@ -1,6 +1,10 @@ +#!/usr/bin/env bash + # Common bash utilities # ---------------------- +# shellcheck disable=SC2034 + # Colors BLACK="0;30" GRAY="1;30" |