aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:22:26 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:22:26 +0200
commit746cee9d2ea090c0b91dc358844f3456b8e91da8 (patch)
tree2eca1b3fdf65d47817718759301eaea4fb909d3a /.gitlab-ci.yml
parent00b000ac303bf41434fae2765d10b0b719260d0c (diff)
downloadcompcert-kvx-746cee9d2ea090c0b91dc358844f3456b8e91da8.tar.gz
compcert-kvx-746cee9d2ea090c0b91dc358844f3456b8e91da8.zip
move check-admitted elsewhere
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml8
1 files changed, 6 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d4578ef..ed3cb261 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,11 +1,15 @@
stages:
- - check-admitted
- build
check-admitted:
- stage: check-admitted
+ stage: build
image: "coqorg/coq"
+ before_script:
+ - opam switch 4.07.1+flambda
+ - eval `opam config env`
+ - opam install -y menhir
script:
+ - ./config_x86_64.sh
- make check-admitted
build_x86_64: