aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-07 14:04:43 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-07 14:04:43 +0100
commit2a59cdce8c142d451988709a3939b884c63993c9 (patch)
tree0b39e900ef744160b8c453bb9f5f017c5d3a8039 /.travis.yml
parentf8c1284a3f5454964aa3002575159b2c9c3df34c (diff)
[travis] [External CI] GeoCoq
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 7529870cd..188e44600 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -28,6 +28,7 @@ env:
- TEST_TARGET="ci-compcert"
- TEST_TARGET="ci-coquelicot"
- TEST_TARGET="ci-cpdt"
+ - TEST_TARGET="ci-geocoq"
- TEST_TARGET="ci-fiat-crypto"
- TEST_TARGET="ci-flocq"
- TEST_TARGET="ci-hott"