From d06497cf329db11309f966821b8727944b452d28 Mon Sep 17 00:00:00 2001 From: Niels de Vos Date: Wed, 7 Aug 2024 13:59:16 +0200 Subject: [PATCH] doc: add description of Mergify commands for merging a PR Signed-off-by: Niels de Vos --- docs/development-guide.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/development-guide.md b/docs/development-guide.md index e9eca403c..2d67eaf37 100644 --- 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