diff options
| author | Emilio Jesus Gallego Arias | 2018-06-13 19:05:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-13 19:05:30 +0200 |
| commit | ae9b65cc27a5a45442502e8119b2d282dcfaa5b4 (patch) | |
| tree | c6482242de75faa551d6a9b9cc392afaca8690c0 /dev | |
| parent | b847fa80a9fdb8c52be32e5e812cfcf3c5ede283 (diff) | |
| parent | 8cc16194852856c542b5bf36b12dd718c8320e18 (diff) | |
Merge PR #7785: Document how to restart failed CI jobs.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/MERGING.md | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 0b4078a7ce..c0cd9c8cdd 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -76,6 +76,16 @@ documentation and test cases. If not, they should leave a comment on the PR and put the approriate label. Otherwise, they are expected to merge the PR using the [merge script](../tools/merge-pr.sh). +When CI has a few failures which look spurious, restarting the corresponding +jobs is a good way of ensuring this was indeed the case. +To restart a job on Travis, you should connect using your GitHub account; +being part of the Coq organization on GitHub should give you the permission +to do so. +To restart a job on GitLab CI, you should sign into GitLab (this can be done +using a GitHub account); if you are part of the +[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" +button; otherwise, send a request to join the organization. + When the PR has conflicts, the assignee can either: - ask the author to rebase the branch, fixing the conflicts - warn the author that they are going to rebase the branch, and push to the |