aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-24 02:28:27 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-24 14:55:15 +0100
commit4567e3a0a44a6c398375effa7d9a49342172512a (patch)
tree1f7bc2c911a49e9bfbb7ef3099fe4940b7e0502c /.travis.yml
parent1682d4ed9df64937dfaa162e58233020036ff7b3 (diff)
[travis] [External CI] fiat-parsers
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 de16f2d0b..5ed0809a5 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -30,6 +30,7 @@ env:
- TEST_TARGET="ci-cpdt"
- 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"