aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-17 12:17:35 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-17 12:17:35 +0200
commit8beb75435a3ffd3c91ad08cd8b2ca42fb2bb5896 (patch)
tree40fafe5a55bff8705cbae1c05f3119b4165c98c7 /.travis.yml
parente09a8cf6a2db97b75796a54296683fe12977d018 (diff)
parentc64a28ee5a6643449f7c77ed7b8737e8f01ede52 (diff)
Merge branch 'v8.6'
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
index 06ce3cae2..aa2e0e63c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -37,6 +37,7 @@ env:
- TEST_TARGET="ci-fiat-crypto"
- TEST_TARGET="ci-fiat-parsers"
- TEST_TARGET="ci-flocq"
+ - TEST_TARGET="ci-formal-topology"
- TEST_TARGET="ci-hott"
- TEST_TARGET="ci-iris-coq"
- TEST_TARGET="ci-math-classes"