From 76abadc18d964850e181e55bfdd55f7c32a3572e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 30 Jul 2020 20:54:39 +0200
Subject: Merging is now possible with coqbot.

This is proposed as an alternative to the merge script, in particular
for maintainers without a GPG key.
---
 CONTRIBUTING.md | 10 ++++++----
 1 file 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
-- 
cgit v1.2.3