diff options
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 |