aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9c1c64a13f..64d930a735 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -690,6 +690,7 @@ library:ci-math-comp:
library:ci-sf:
extends: .ci-template
+ allow_failure: true # Waiting for integration of the fix for #10476
library:ci-stdlib2:
extends: .ci-template-flambda