aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 17:17:28 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-22 17:22:12 +0100
commit1b0d67a0cf1b725715e97ba6448c3ff0154813bc (patch)
tree7cba9bed3fd3266c2938e292734ff7c357900877 /.travis.yml
parentcd87eac3757d8925ff4ba7dee85efadb195153a3 (diff)
[travis] [8.6.only] Backport latest changes from trunk.
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml4
1 files changed, 4 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
index f609852bc..7138d5c61 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,4 +1,7 @@
dist: trusty
+# Travis builds are slower using sudo: false (the container-based
+# infrastructure) as of March 2017; see
+# https://github.com/coq/coq/pull/467 for some discussion.
sudo: required
# Until Ocaml becomes a language, we set a known one.
language: c
@@ -29,6 +32,7 @@ env:
- TEST_TARGET="ci-coquelicot"
- TEST_TARGET="ci-geocoq"
- TEST_TARGET="ci-fiat-crypto"
+ - TEST_TARGET="ci-fiat-parsers"
- TEST_TARGET="ci-flocq"
- TEST_TARGET="ci-hott"
- TEST_TARGET="ci-iris-coq"