duneci-standard-test: use /duneci/opts.gcc by default

Otherwise no opts file is used at all and the code is built without any
optimization, leading to timeouts in tests.
parent 60d22974
Pipeline #567 canceled with stages
in 13 minutes and 50 seconds
......@@ -3,7 +3,7 @@
set -e
set -u
if [[ -n "${DUNECI_OPTS:-}" ]]; then
if [[ -n "${DUNECI_OPTS:-/duneci/opts.gcc}" ]]; then
set -- --opts="${DUNECI_OPTS}" "${@}"
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment