From 040890448b2ead3ae67c1f514514955da784ec52 Mon Sep 17 00:00:00 2001
From: "Michael B. Gale" <mbg@github.com>
Date: Thu, 22 Oct 2026 14:47:35 +0100
Subject: [PATCH] Add workflow to comment on a PR when it was dequeued

---
 .github/workflows/pr-dequeued.yml | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 .github/workflows/pr-dequeued.yml

diff --git a/.github/workflows/pr-dequeued.yml b/.github/workflows/pr-dequeued.yml
new file mode 100644
index 000000000..7d39ef97e
--- /dev/null
+++ b/.github/workflows/pr-dequeued.yml
@@ -0,0 +1,28 @@
+name: PR dequeued
+
+on:
+  pull_request:
+    types:
+      - dequeued
+
+jobs:
+  notify:
+    name: Notify
+    runs-on: ubuntu-slim
+
+    if: github.event.pull_request.merged != true
+
+    permissions:
+      pull-requests: write
+
+    steps:
+      - name: Notify that the PR was removed from the merge queue
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+          REASON: ${{ github.event.reason }}
+          SENDER: ${{ github.event.sender.login }}
+        run: |
+          echo "@$SENDER The pull request was removed from the merge queue (\`$REASON\`)." \
+            "Please resolve any issues if required and enqueue the PR again." |
+            gh pr comment --body-file - --repo github/codeql-action "$PR_NUMBER"