aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-10 15:10:15 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-10 15:10:15 +0200
commit70bf549f1c790969430f505c004b48637fef244e (patch)
tree94c3591e53366cb385fc4140b60269ce37d002d8
parent38d4b5cba84a253f2f4ea4febda9f60fde2052c9 (diff)
Remove auto-retry in GitLab CI now that @coqbot is handling it.
-rw-r--r--.gitlab-ci.yml1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 11614bc38..7c451af26 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -55,7 +55,6 @@ after_script:
# TODO figure out how to build doc for installed Coq
.build-template: &build-template
stage: build
- retry: 1
artifacts:
name: "$CI_JOB_NAME"
paths: