From 88a6867adae0e4a4cf629b3f782d365f62fdb647 Mon Sep 17 00:00:00 2001
From: Markus Rudy <mr@edgeless.systems>
Date: Sun, 17 Nov 2024 15:16:44 +0100
Subject: [PATCH] ci: prevent merge of PRs with do-not-merge label

---
 .github/workflows/require_label.yml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/.github/workflows/require_label.yml b/.github/workflows/require_label.yml
index 38df65515b..ea847fb225 100644
--- a/.github/workflows/require_label.yml
+++ b/.github/workflows/require_label.yml
@@ -22,3 +22,13 @@ jobs:
             feature
             documentation
             no changelog
+  do-not-merge:
+    if: ${{ contains(github.event.pull_request.labels.*.name, 'do not merge') }}
+    runs-on: ubuntu-22.04
+    steps:
+      - name: prevent merge
+        run: |
+          tee "${GITHUB_STEP_SUMMARY}" <<'EOF'
+          This PR is labeled as `do not merge`, remove the label to make this check pass.
+          EOF
+          exit 1