aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:20:05 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-31 19:20:05 +0200
commit00b000ac303bf41434fae2765d10b0b719260d0c (patch)
tree8e9087bb6acfa74ddbcef674ffcb1f200d3820ae /.gitlab-ci.yml
parentaad09479f2ae3e008cbe38ca4fa0e8e3e04daec9 (diff)
downloadcompcert-kvx-00b000ac303bf41434fae2765d10b0b719260d0c.tar.gz
compcert-kvx-00b000ac303bf41434fae2765d10b0b719260d0c.zip
forgot image
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4c00848f..7d4578ef 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,6 +4,7 @@ stages:
check-admitted:
stage: check-admitted
+ image: "coqorg/coq"
script:
- make check-admitted