aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml13
1 files changed, 13 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 309044a1e9..8dafb8d5fd 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
@@ -506,6 +512,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 +541,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