diff options
| author | coqbot-app[bot] | 2020-08-25 10:15:26 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-25 10:15:26 +0000 |
| commit | ae7e82a5873de2cc4fdbfd0d10e0fa3961146ffd (patch) | |
| tree | 8c5d71409f2f61b68cf5d1ff92a47381fca67528 | |
| parent | bd4791ff350bef9dc45b42b2ae77769625644c4f (diff) | |
| parent | 76abadc18d964850e181e55bfdd55f7c32a3572e (diff) | |
Merge PR #12778: Merging is now possible with coqbot.
Reviewed-by: ejgallego
| -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 |