aboutsummaryrefslogtreecommitdiff
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-05-06 22:17:10 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-06-17 13:00:26 -0400
commit037df57566b1108af0d13cfcafe9b0f8fdd5937b (patch)
tree9310260156d8d1e19215fb4765b5a4e64dc9a9d2 /.travis.yml
parenta073821cf7ba0714a30e892af40bd309cd5f2f03 (diff)
New pipeline, split among files
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml7
1 files changed, 7 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
index cc2c9a0c5..71d5315a4 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -122,6 +122,13 @@ jobs:
env: COQ_VERSION="8.7.2" COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
script: PREV=3 CUR=4 ./etc/ci/travis.sh build-selected-test build-selected-bench
+ - stage: standalone-ocaml
+ env: COQ_VERSION="8.8.0" COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
+ script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml
+ - stage: standalone-ocaml
+ env: COQ_VERSION="8.7.2" COQ_PACKAGE="coq-8.7.2" PPA="ppa:jgross-h/many-coq-versions"
+ script: PREV=4 CUR=5 ./etc/ci/travis.sh standalone-ocaml
+
# - stage: selected-test selected-bench
# env: COQ_VERSION="8.8.0" COQ_PACKAGE="coq-8.8.0" PPA="ppa:jgross-h/many-coq-versions"
# allow_failure: true