diff options
| author | Emilio Jesus Gallego Arias | 2021-03-11 17:19:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2021-03-14 01:35:08 +0100 |
| commit | f4579a0bcdbdba6304a9970fc6ea6190a68f9c8c (patch) | |
| tree | d68f8f0167bc0f36333428f6d224d4f61df569c0 /.gitlab-ci.yml | |
| parent | def498d87d9ad43e43bd8e6e70b8d8f6ae9272be (diff) | |
[ci] [gitlab] Remove ad-hoc mathcomp install macros
They should not be necessary today as they date from the shareable
pre-artifact epoch, an incur in an slowdown.
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a8bca2bffe..ce6be777f3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -706,7 +706,11 @@ library:ci-engine_bench: extends: .ci-template library:ci-fcsl_pcm: - extends: .ci-template + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp library:ci-fiat_crypto: extends: .ci-template-flambda @@ -781,6 +785,10 @@ plugin:ci-gappa: library:ci-geocoq: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp library:ci-hott: extends: .ci-template @@ -878,6 +886,10 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp plugin:ci-reduction_effects: extends: .ci-template |