diff options
Diffstat (limited to '.gitlab/ci.sh')
| -rwxr-xr-x | .gitlab/ci.sh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index 94be278aa1..92a878546f 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -448,7 +448,7 @@ function test_make() { } function build_hadrian() { - if [ -z "$BIN_DIST_NAME" ]; then + if [ -z "${BIN_DIST_NAME:-}" ]; then fail "BIN_DIST_NAME not set" fi @@ -526,7 +526,7 @@ function clean() { } function run_hadrian() { - if [ -z "$BUILD_FLAVOUR" ]; then + if [ -z "${BUILD_FLAVOUR:-}" ]; then fail "BUILD_FLAVOUR not set" fi if [ -z "${BIGNUM_BACKEND:-}" ]; then BIGNUM_BACKEND="gmp"; fi @@ -537,7 +537,7 @@ function run_hadrian() { -j"$cores" \ --broken-test="${BROKEN_TESTS:-}" \ --bignum=$BIGNUM_BACKEND \ - "${args[@]}" \ + "${args[@]+"${args[@]}"}" \ "$@" } |