diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-27 14:31:45 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-28 12:30:27 +0100 |
| commit | 3b0fc06ccc21f23df111d59cccd1e5ecae4de919 (patch) | |
| tree | a64adb2f4b574d813b401b0fab140ead1175b06a /.travis.yml | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Travis: do not build stdlib in [warnings] jobs.
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/.travis.yml b/.travis.yml index 1f6bb11e0..44c799c71 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ env: - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" - COQ_DEST="-local" + - MAIN_TARGET="world" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -139,7 +140,7 @@ matrix: # Ocaml warnings with two compilers - env: - - TEST_TARGET="coqocaml" + - MAIN_TARGET="coqocaml" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target @@ -155,7 +156,7 @@ matrix: - libgtksourceview2.0-dev - env: - - TEST_TARGET="coqocaml" + - MAIN_TARGET="coqocaml" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" @@ -224,11 +225,11 @@ script: - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' -- make -j ${NJOBS} +- make -j ${NJOBS} ${MAIN_TARGET} - echo -en 'travis_fold:end:coq.build\\r' - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' -- ${TW} make -j ${NJOBS} ${TEST_TARGET} +- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi - echo -en 'travis_fold:end:coq.test\\r' - set +e |