aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
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 491a6c424..5cae5fcd3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -63,6 +63,7 @@ env:
matrix:
allow_failures:
+ - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
- env: TEST_TARGET="ci-geocoq"
include: