diff --git a/base-common/duneci-standard-test b/base-common/duneci-standard-test index 2a93e6d6425bd86fd6735e498511a1a39260e882..9f4bf1d6781425a64826758b63646557be3a2a46 100755 --- a/base-common/duneci-standard-test +++ b/base-common/duneci-standard-test @@ -3,9 +3,8 @@ set -e set -u -if [[ -n "${DUNECI_OPTS:-/duneci/opts.gcc}" ]]; then - set -- --opts="${DUNECI_OPTS}" "${@}" -fi +: ${DUNECI_OPTS:=/duneci/opts.gcc} +set -- --opts="${DUNECI_OPTS}" "${@}" DUNECONTROL=dunecontrol if [[ -x bin/dunecontrol ]]; then