aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-18 13:28:06 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-18 13:28:06 +0200
commita93d65fa0b48525f54c4474c07dc06ca00f4adc8 (patch)
tree667985d20a8273beb4077ac15f03f90519500186 /.travis.yml
parent46c00567cc609fda60ea26a29dc1283e5d1f96a3 (diff)
Separate jobs for test-suite and package building under OSX.
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml16
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)