diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-14 04:20:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-14 04:22:39 +0200 |
commit | 6bf8018c3d1fdfff974d0e83913bb3a42281b01e (patch) | |
tree | b6744b2a4a34c4c850c26c7a05d670977daa7270 /.circleci | |
parent | 12109393c957ef64f7dc8d47b745a75392e4382c (diff) |
[ci] [circleci] Remove jobs done in Gitlab efficiently.
Following the migration to Gitlab (#6919) we reduce Circle load, see
also discussion in #7436 and #7482.
Diffstat (limited to '.circleci')
-rw-r--r-- | .circleci/config.yml | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 14c102ced..79f83d472 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -160,22 +160,22 @@ workflows: requires: - build - bignums - - compcert: *req-main - - coq-dpdgraph: *req-main - - coquelicot: *req-main - - cross-crypto: *req-main - - elpi: *req-main - - equations: *req-main - - geocoq: *req-main - - fcsl-pcm: *req-main - - fiat-crypto: *req-main - - fiat-parsers: *req-main - - flocq: *req-main + # - compcert: *req-main + # - coq-dpdgraph: *req-main + # - coquelicot: *req-main + # - cross-crypto: *req-main + # - elpi: *req-main + # - equations: *req-main + # - geocoq: *req-main + # - fcsl-pcm: *req-main + # - fiat-crypto: *req-main + # - fiat-parsers: *req-main + # - flocq: *req-main - math-classes: requires: - build - bignums - - mtac2: *req-main + # - mtac2: *req-main - corn: requires: - build @@ -184,11 +184,11 @@ workflows: requires: - build - corn - - hott: *req-main - - iris-lambda-rust: *req-main - - ltac2: *req-main - - math-comp: *req-main - - pidetop: *req-main - - sf: *req-main - - unimath: *req-main - - vst: *req-main + # - hott: *req-main + # - iris-lambda-rust: *req-main + # - ltac2: *req-main + # - math-comp: *req-main + # - pidetop: *req-main + # - sf: *req-main + # - unimath: *req-main + # - vst: *req-main |