aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-03 14:05:47 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-10-03 14:05:47 +0200
commit0fe3775278112621f1c9cbf76282a20f48bec8d1 (patch)
treec5fd936427b7e4069f4e48a687697d5b075cdbd9
parent536053ed6f114905c3e594b789ed9456b1fcb99a (diff)
Remove GeoCoq from allowed failures.
-rw-r--r--.travis.yml3
1 files changed, 0 insertions, 3 deletions
diff --git a/.travis.yml b/.travis.yml
index 6c926aacb..8d85ffc68 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -62,9 +62,6 @@ env:
matrix:
- allow_failures:
- - env: TEST_TARGET="ci-geocoq TIMED=1"
-
include:
# Full Coq test-suite with two compilers
- env: