diff options
| -rwxr-xr-x | .gitlab/ci.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/.gitlab/ci.sh b/.gitlab/ci.sh index 8734c975f4..95460e4f1e 100755 --- a/.gitlab/ci.sh +++ b/.gitlab/ci.sh @@ -363,9 +363,11 @@ function configure() { fi start_section "configuring" + # See https://stackoverflow.com/questions/7577052 for a rationale for the + # args[@] symbol-soup below. run ./configure \ --enable-tarballs-autodownload \ - "${args[@]}" \ + "${args[@]+"${args[@]}"}" \ GHC="$GHC" \ HAPPY="$HAPPY" \ ALEX="$ALEX" \ |