aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-08-24 12:50:34 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-08-24 12:52:53 -0400
commit2e9aa9329b598ce7fe5be469dda78a380309a3b2 (patch)
treea786a0c6b59ca50c7c2649e1e93ebadbc177fa20 /.gitlab-ci.yml
parent574cdd8674750b7ed114ff0fb8730f4ebdd0d4b2 (diff)
[ci] [gitlab] coq-dpdgraph: Remove allow-failure
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b47494d3a..8beeffcca 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