doc: add description of Mergify commands for merging a PR

Signed-off-by: Niels de Vos <ndevos@ibm.com>
ceph · Aug 7, 2024 · f92edd6 · f92edd6
1 parent b40a6c0
commit f92edd6
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/docs/development-guide.md b/docs/development-guide.md
@@ -278,8 +278,11 @@ need to be met before it will be merged:
   on the PR. The bot will merge the PR if it's having one approval and the
   label `ready-to-merge`.
 
-When the criteria are met, a project maintainer can merge your changes into
-the project's devel branch.
+When the criteria are met, a project maintainer can instruct the Mergify bot to
+queue the PR for merging. This usually is done by leaving two comments:
+
+* `@mergifyio rebase` to rebase on the latest HEAD of the branch
+* `@mergifyio queue` once the rebasing is done, to add the PR to the merge queue
 
 ### Backport a Fix to a Release Branch