aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2019-10-08 10:11:06 +0200
committerCyril Cohen2019-12-11 14:26:52 +0100
commitf8d7a9f1090785a61dd81d745a0f46a24515f3d8 (patch)
tree00a11f85a2f5f4a49a9b59a26a0415b4ee57a041 /.gitlab-ci.yml
parentb0a01acd904cbfcaf47d821b3b5e72098b9efb07 (diff)
Rename `totalLatticeMixin` to `totalPOrderMixin` and several refactor
- Rename `totalLatticeMixin` to `totalPOrderMixin`. - Refactor num mixins. - Use `Num.min` and `Num.max` rather than lattice notations if applicable.
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml8
1 files changed, 4 insertions, 4 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b366d39..3a94cf1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -145,7 +145,7 @@ coq-dev:
- make install
except:
- /^experiment\/order$/
- - /^pr-(270|383)$/
+ - /^pr-(270|388|389)$/
ci-fourcolor-8.7:
extends: .ci-fourcolor
@@ -182,7 +182,7 @@ ci-fourcolor-dev:
- make install
only:
- /^experiment\/order$/
- - /^pr-(270|383)$/
+ - /^pr-(270|388|389)$/
ci-fourcolor-8.7-270:
extends: .ci-fourcolor-270
@@ -210,7 +210,7 @@ ci-fourcolor-dev-270:
- make install
except:
- /^experiment\/order$/
- - /^pr-(270|383)$/
+ - /^pr-(270|388|389)$/
ci-odd-order-8.7:
extends: .ci-odd-order
@@ -247,7 +247,7 @@ ci-odd-order-dev:
- make install
only:
- /^experiment\/order$/
- - /^pr-(270|383)$/
+ - /^pr-(270|388|389)$/
ci-odd-order-8.7-270:
extends: .ci-odd-order-270