aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-31 11:38:00 +0200
committerMaxime Dénès2017-08-31 11:38:00 +0200
commit2c50427e59f932f26a8b643ea30c158c5deb432a (patch)
treedaf8f635e9e5ce9f73dc7163315fbb8949ecf5b6
parentc082e2bf85d5e372497a85424a3f1a049862467d (diff)
parent2e9aa9329b598ce7fe5be469dda78a380309a3b2 (diff)
Merge PR #971: Don't allow coq-dpdgraph to fail
-rw-r--r--.gitlab-ci.yml1
-rw-r--r--.travis.yml1
2 files changed, 0 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b47494d3ae..8beeffccac 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -269,7 +269,6 @@ ci-coq-dpdgraph:
<<: *ci-template-vars
EXTRA_OPAM: "ocamlgraph"
EXTRA_PACKAGES: "autoconf"
- allow_failure: true
ci-coquelicot:
<<: *ci-template
diff --git a/.travis.yml b/.travis.yml
index 22715eec20..2d6d9a2a68 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -63,7 +63,6 @@ env:
matrix:
allow_failures:
- - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
- env: TEST_TARGET="ci-geocoq TIMED=1"
include: