diff options
| author | Emilio Jesus Gallego Arias | 2018-07-11 00:54:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-11 00:54:54 +0200 |
| commit | 8fead59914019aac5951ff123f806f69ceb30ccb (patch) | |
| tree | 89ac61d9783a3e0bf554a20f8177858498accf12 | |
| parent | b4572185522cd21e7e4e1cf59095ae66d0da0be1 (diff) | |
| parent | 70bf549f1c790969430f505c004b48637fef244e (diff) | |
Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.
| -rw-r--r-- | .gitlab-ci.yml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 11614bc380..7c451af26d 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: |