Skip to content
Snippets Groups Projects
Commit c2506dd1 authored by René Fritze's avatar René Fritze
Browse files

Revert "[travis] mixed up opts location"

This was not actually the issue.
This reverts commit 13227922cb6f9ed1ff628c9b17753cfc4e7045b2.
parent 1c9918b0
No related branches found
No related tags found
No related merge requests found
......@@ -22,7 +22,7 @@ addons:
before_install:
- |-
: ${OPTS:="travis.ninja"}
: ${OPTS:="config.opts/travis.ninja"}
- |-
: ${MAKE:="ninja"}
# workaround for https://github.com/travis-ci/travis-ci/issues/5285
......@@ -37,7 +37,7 @@ before_install:
- cd $HOME/src
- git submodule update --init --recursive
- git submodule status
- export DCTRL_ARG="--builddir=${DUNE_BUILD_DIR} --opts=config.opts/${OPTS}"
- export DCTRL_ARG="--builddir=${DUNE_BUILD_DIR} --opts=${OPTS}"
# our local scripts look for an OPTS env entry
- ./local/bin/download_external_libraries.py
- ./local/bin/build_external_libraries.py
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment