diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6afe3bd0a8..f17e06b520 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -592,6 +592,7 @@ library:ci-coqprime: - build:edge+flambda - plugin:ci-bignums dependencies: + - build:edge+flambda - plugin:ci-bignums library:ci-coquelicot: @@ -613,6 +614,7 @@ library:ci-fiat-crypto: - plugin:ci-bignums - plugin:ci-rewriter dependencies: + - build:edge+flambda - library:ci-bedrock2 - library:ci-coqprime - plugin:ci-rewriter |