diff options
| author | Gaetan Gilbert | 2017-05-05 13:19:21 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-05-17 09:12:40 +0200 |
| commit | f6b0d8b78ae25c8b1c6b901e57a5f4e38f20cdbd (patch) | |
| tree | e9f888c0fc0aaa8febd6fc6f19e971a7ab8dbe9c | |
| parent | 5360ec8ff56c44e96c56965be78e6f2538963a57 (diff) | |
Travis: do not run the tests if building Coq fails
| -rw-r--r-- | .travis.yml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index 5604551879..8dcc34a8d2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -115,6 +115,7 @@ install: script: +- set -e - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' - ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' @@ -126,6 +127,7 @@ script: - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' - ${TW} make -j ${NJOBS} ${TEST_TARGET} - echo -en 'travis_fold:end:coq.test\\r' +- set +e # Testing Gitter webhook notifications: |