diff options
| author | Emilio Jesus Gallego Arias | 2020-07-15 11:26:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-15 11:26:04 +0200 |
| commit | d0cfc7a14318448f9b5c8706bd876fa258d97c9d (patch) | |
| tree | 3378d57b1903efffb35818eac2892f7ae3e35e87 | |
| parent | bcccf103bc714c57485fc82ccb7504ada8fcc737 (diff) | |
| parent | 5a6afa0acfdf575b818d7d88588cb2fad5b813b8 (diff) | |
Merge PR #12673: Fix fiat_crypto(_ocaml) needs/dependencies
Reviewed-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 819ad8a214..3b95800f0d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -751,6 +751,7 @@ library:ci-fiat_crypto: dependencies: - build:edge+flambda - library:ci-coqprime + - plugin:ci-bignums - plugin:ci-rewriter library:ci-fiat_crypto_legacy: @@ -765,9 +766,15 @@ library:ci-fiat_crypto_ocaml: stage: stage-5 needs: - build:edge+flambda + - library:ci-coqprime + - plugin:ci-bignums + - plugin:ci-rewriter - library:ci-fiat_crypto dependencies: - build:edge+flambda + - library:ci-coqprime + - plugin:ci-bignums + - plugin:ci-rewriter - library:ci-fiat_crypto library:ci-flocq: |