aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authoraffeldt-aist2019-11-14 20:49:44 +0900
committerCyril Cohen2019-12-11 14:26:52 +0100
commitb3261c9020105f3c6667697b22ca8a542271bc4c (patch)
treef7c6918d64decf70ce01d0bf5d21e868532402a8 /.gitlab-ci.yml
parent050ad8395fb250e9396b7a376a75c523567e177c (diff)
renaming NormedZmoduleType and NormedZmoduleMixin (#416)
* renaming NormedZmoduleType -> NormedZmodType NormedZmoduleMixin -> NormedZmodMixin that looks more homogeneous with regard to naming conventions used so far * update .gitlab-ci.yml * typo
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 87befed..3b83fea 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -145,7 +145,7 @@ coq-dev:
- make install
except:
- /^experiment\/order$/
- - /^pr-(270|388|402)$/
+ - /^pr-(270|388|402|416)$/
ci-fourcolor-8.7:
extends: .ci-fourcolor
@@ -182,7 +182,7 @@ ci-fourcolor-dev:
- make install
only:
- /^experiment\/order$/
- - /^pr-(270|388|402)$/
+ - /^pr-(270|388|402|416)$/
ci-fourcolor-8.7-270:
extends: .ci-fourcolor-270
@@ -210,7 +210,7 @@ ci-fourcolor-dev-270:
- make install
except:
- /^experiment\/order$/
- - /^pr-(270|388|402)$/
+ - /^pr-(270|388|402|416)$/
ci-odd-order-8.7:
extends: .ci-odd-order
@@ -247,7 +247,7 @@ ci-odd-order-dev:
- make install
only:
- /^experiment\/order$/
- - /^pr-(270|388|402)$/
+ - /^pr-(270|388|402|416)$/
ci-odd-order-8.7-270:
extends: .ci-odd-order-270