diff options
| author | Théo Zimmermann | 2020-07-30 20:54:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-07-30 20:54:39 +0200 |
| commit | 76abadc18d964850e181e55bfdd55f7c32a3572e (patch) | |
| tree | 847c742ffc68ab272226826f86b84786fd8f6f49 | |
| parent | e0b8b4684eaf76f897ac708ffddbb8e4977ac754 (diff) | |
Merging is now possible with coqbot.
This is proposed as an alternative to the merge script, in particular
for maintainers without a GPG key.
| -rw-r--r-- | CONTRIBUTING.md | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d561ec8a12..a96b93154c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -791,10 +791,12 @@ organization, because of a limitation of GitHub). #### Additional notes for pull request reviewers and assignees #### -- NEVER USE GITHUB'S MERGE BUTTON. Instead, we provide a script - [`dev/tools/merge-pr.sh`][merge-pr] which you should use to merge a - PR (requires having configured gpg with git). In the future, we - will also support merging through a command to **@coqbot**. +- NEVER USE GITHUB'S MERGE BUTTON. Instead, you should either: + - run the [`dev/tools/merge-pr.sh`][merge-pr] script (requires + having configured gpg with git); + - or post a comment containing "@coqbot: merge now" (this is + especially convenient for developers who do not have a GPG key and + for when you do not have access to a console). - PR authors or co-authors cannot review, self-assign, or merge the PR they contributed to. However, reviewers may push small fixes to the |