aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 20:27:38 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 20:27:38 +0200
commited2e43e3513aa6950480015b255af69df4d86ab9 (patch)
tree51f0b16c939df7d99d5bdd34c703b266c5cacb09
parentfdfb99dcd5a5d1a70d2755943ce3cdac540eeae2 (diff)
parent746cee9d2ea090c0b91dc358844f3456b8e91da8 (diff)
downloadcompcert-kvx-ed2e43e3513aa6950480015b255af69df4d86ab9.tar.gz
compcert-kvx-ed2e43e3513aa6950480015b255af69df4d86ab9.zip
Merge remote-tracking branch 'origin/mppa-work' into mppa-licm
-rw-r--r--.gitlab-ci.yml11
1 files changed, 11 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 79a32b25..ed3cb261 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,6 +1,17 @@
stages:
- build
+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:
stage: build
image: "coqorg/coq"