From d086c6c6b3f8b2661596f1d424871601e7c5a96f Mon Sep 17 00:00:00 2001
From: Wolfgang Walther <walther@technowledgy.de>
Date: Thu, 6 Nov 2025 12:51:46 +0100
Subject: [PATCH] ci/github-script/merge: add hint about stuck GitHub

Unfortunately it still happens frequently that, after enabling
auto-merge, GitHub is stuck even though all checks have passed, and
doesn't merge the PR. Any contributor can trigger GitHub again with an
approval of the PR - this will then immediately queue the PR for merge.

Adding a hint to the posted comment, should help users through this
without my intervention.
---
 ci/github-script/merge.js | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/ci/github-script/merge.js b/ci/github-script/merge.js
index 688a7928fe97..deb2b5bdabba 100644
--- a/ci/github-script/merge.js
+++ b/ci/github-script/merge.js
@@ -182,7 +182,9 @@ async function handleMerge({
         }`,
         { node_id: pull_request.node_id, sha: pull_request.head.sha },
       )
-      return `[Queued](${resp.enqueuePullRequest.mergeQueueEntry.mergeQueue.url}) for merge`
+      return [
+        `:heavy_check_mark: [Queued](${resp.enqueuePullRequest.mergeQueueEntry.mergeQueue.url}) for merge (#306934)`,
+      ]
     } catch (e) {
       log('Enqueing failed', e.response.errors[0].message)
     }
@@ -201,7 +203,12 @@ async function handleMerge({
         }`,
         { node_id: pull_request.node_id, sha: pull_request.head.sha },
       )
-      return 'Enabled Auto Merge'
+      return [
+        `:heavy_check_mark: Enabled Auto Merge (#306934)`,
+        '',
+        '> [!TIP]',
+        '> Sometimes GitHub gets stuck after enabling Auto Merge. In this case, leaving another approval should trigger the merge.',
+      ]
     } catch (e) {
       log('Auto Merge failed', e.response.errors[0].message)
       throw new Error(e.response.errors[0].message)
@@ -287,7 +294,7 @@ async function handleMerge({
     if (result) {
       await react('ROCKET')
       try {
-        body.push(`:heavy_check_mark: ${await merge()} (#306934)`)
+        body.push(...(await merge()))
       } catch (e) {
         // Remove the HTML comment with node_id reference to allow retrying this merge on the next run.
         body.shift()