diff options
| author | Gaëtan Gilbert | 2017-06-16 11:02:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-06-16 12:33:21 +0200 |
| commit | 7eed898a0418fba38821594efe8f98a458d8bb10 (patch) | |
| tree | ff000b4a621bbed35d56eefa6c8dbb216b6713ad | |
| parent | da0459552dd4ac253e45bb519d99a5a718105313 (diff) | |
Add coq-dpdgraph to gitlab CI
| -rw-r--r-- | .gitlab-ci.yml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d5351f5738..92243b7573 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -259,6 +259,14 @@ ci-color: ci-compcert: <<: *ci-template +ci-coq-dpdgraph: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_OPAM: "ocamlgraph" + EXTRA_PACKAGES: "autoconf" + allow_failure: true + ci-coquelicot: <<: *ci-template variables: |