diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-18 13:28:06 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-18 13:28:06 +0200 |
commit | a93d65fa0b48525f54c4474c07dc06ca00f4adc8 (patch) | |
tree | 667985d20a8273beb4077ac15f03f90519500186 | |
parent | 46c00567cc609fda60ea26a29dc1283e5d1f96a3 (diff) |
Separate jobs for test-suite and package building under OSX.
-rw-r--r-- | .travis.yml | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/.travis.yml b/.travis.yml index 66befc48c..7a0e80b54 100644 --- a/.travis.yml +++ b/.travis.yml @@ -140,9 +140,20 @@ matrix: env: - TEST_TARGET="test-suite" - COMPILER="4.02.3" + - CAMLP5_VER="6.17" + - NATIVE_COMP="no" + - COQ_DEST="-local" + before_install: + - brew update + - brew install opam gnu-time + + - os: osx + env: + - TEST_TARGET="" + - COMPILER="4.02.3" - CAMLP5_VER="6.17" - NATIVE_COMP="no" - - COQ_DEST="-prefix _install" + - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="lablgtk-extras" before_install: @@ -161,6 +172,9 @@ matrix: on: all_branches: true +before_install: +- if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi + install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) |