aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml14
1 files changed, 14 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 58bf6bf065..fd94051a37 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -253,6 +253,9 @@ build:base+async:
COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
COQUSERFLAGS: "-async-proofs on"
allow_failure: true # See https://github.com/coq/coq/issues/9658
+ only:
+ variables:
+ - $UNRELIABLE =~ /enabled/
build:quick:
extends: .build-template
@@ -260,6 +263,9 @@ build:quick:
COQ_EXTRA_CONF: "-native-compiler no"
QUICK: "1"
allow_failure: true # See https://github.com/coq/coq/issues/9637
+ only:
+ variables:
+ - $UNRELIABLE =~ /enabled/
windows64:
extends: .windows-template
@@ -351,6 +357,7 @@ pkg:nix:deploy:channel:
script:
- echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
- git fetch --unshallow
+ - git branch -v
- git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_REF_NAME}"
pkg:nix:
@@ -506,6 +513,10 @@ test-suite:base+async:
- build:base
variables:
COQFLAGS: "-async-proofs on"
+ allow_failure: true
+ only:
+ variables:
+ - $UNRELIABLE =~ /enabled/
validate:base:
extends: .validate-template
@@ -531,6 +542,9 @@ validate:quick:
extends: .validate-template
dependencies:
- build:quick
+ only:
+ variables:
+ - $UNRELIABLE =~ /enabled/
# Libraries are by convention the projects that depend on Coq
# but not on its ML API