diff options
| author | Enrico Tassi | 2020-11-24 09:46:54 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-25 15:59:42 +0100 |
| commit | dc8e605d9cadf0d7ead78481e0e68756713f7aa0 (patch) | |
| tree | e24089d1b512f080c5cfaa03a235715fdfd669a8 /.gitlab-ci.yml | |
| parent | 94abc3dce396b77e98900e604e3117986dd2ab60 (diff) | |
[ci] make compcert use flocq and menhir
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7dd9a37f59..3c09d0a8c8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -711,7 +711,12 @@ library:ci-color: - plugin:ci-bignums library:ci-compcert: + stage: stage-3 extends: .ci-template-flambda + needs: + - build:edge+flambda + - library:ci-flocq + - library:ci-menhir library:ci-coq_performance_tests: extends: .ci-template |