From 402b41c1257ffc7cb88f2876b5fa20ab3ffe4f95 Mon Sep 17 00:00:00 2001
From: Wolfgang Walther <walther@technowledgy.de>
Date: Sat, 18 Oct 2025 00:20:49 +0200
Subject: [PATCH] ci/github-script/labels: close empty PRs

If the change of a PR has already been merged to the target branch
elsewhere, the PR will not be auto-closed by GitHub - and will still
show the same original diff. Still, the temporary merge commit is
actually empty. This causes all kinds of strange CI behavior, from not
showing rebuilds to not pinging maintainers.

We check the merge commit during labeling anyway, to see whether a merge
conflict is present. It's easy to just look a the number of affected
files in this merge commit - and if there are none, we can just
automatically close the PR as no longer relevant.
---
 ci/github-script/labels.js | 40 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/ci/github-script/labels.js b/ci/github-script/labels.js
index faf7693c0f04..c57a9bb60a56 100644
--- a/ci/github-script/labels.js
+++ b/ci/github-script/labels.js
@@ -20,6 +20,46 @@ module.exports = async ({ github, context, core, dry }) => {
       })
     ).data
 
+    // When the same change has already been merged to the target branch, a PR will still be
+    // open and display the same changes - but will not actually have any effect. This causes
+    // strange CI behavior, because the diff of the merge-commit is empty, no rebuilds will
+    // be detected, no maintainers pinged.
+    // We can just check the temporary merge commit, and if it's empty the PR can safely be
+    // closed - there are no further changes.
+    if (pull_request.merge_commit_sha) {
+      const commit = (
+        await github.rest.repos.getCommit({
+          ...context.repo,
+          ref: pull_request.merge_commit_sha,
+        })
+      ).data
+
+      if (commit.files.length === 0) {
+        const body = [
+          `The diff for the temporary merge commit ${pull_request.merge_commit_sha} is empty.`,
+          'The changes in this PR have almost certainly already been merged to the target branch.',
+        ].join('\n')
+
+        core.info(`PR #${item.number}: closed`)
+
+        if (!dry) {
+          await github.rest.issues.createComment({
+            ...context.repo,
+            issue_number: pull_number,
+            body,
+          })
+
+          await github.rest.pulls.update({
+            ...context.repo,
+            pull_number,
+            state: 'closed',
+          })
+        }
+
+        return {}
+      }
+    }
+
     const reviews = await github.paginate(github.rest.pulls.listReviews, {
       ...context.repo,
       pull_number,