aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 11:45:45 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 11:45:45 +0200
commitc5dabed1c1f33005fe942882ea0fcf008d52784a (patch)
tree2d892ec15b5fc0e59acc20d766128de47f7b3528 /.gitlab-ci.yml
parent929dc481c91dc860b69b08dd65fb6f65d5650e23 (diff)
Remove bedrock from test suite.
Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq.
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml6
1 files changed, 0 insertions, 6 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d5351f573..1de9e7f7c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -244,12 +244,6 @@ validate:32bit:
ci-bignums:
<<: *ci-template
-ci-bedrock-src:
- <<: *ci-template
-
-ci-bedrock-facade:
- <<: *ci-template
-
ci-color:
<<: *ci-template
variables: