Add CI section; document PipelineRetry command (#1149)

This commit is contained in:
Andrew David Wong 2021-06-27 22:35:56 -07:00
parent 1c5aab4340
commit decc4135f9
No known key found for this signature in database
GPG Key ID: 8CE137352A019A17

View File

@ -576,3 +576,14 @@ Here's an example that follows the indentation rules:
Please try to write good commit messages, according to the [instructions in our
coding style guidelines](/doc/coding-style/#commit-message-guidelines).
## Continuous Integration (CI)
The following commands may be useful as a way to interact with our CI
infrastructure. Note that special permissions may be required to use some of
these commands. These commands are generally issued by adding a comment to a
pull request (PR) containing only the command.
- `PipelineRetry`: Attempts to run the entire build pipeline over again. This
can be useful if CI incorrectly uses a stale branch instead of testing the PR
as if it were merged into `master`.