From 207fbc88f1550974ee87d207cf554a87e455543a 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

Co-authored-by: Paul Meyer <49727155+katexochen@users.noreply.github.com>
---
 .github/workflows/require_label.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/require_label.yml b/.github/workflows/require_label.yml
index 38df65515b..5ee13e4e0f 100644
--- a/.github/workflows/require_label.yml
+++ b/.github/workflows/require_label.yml
@@ -22,3 +22,11 @@ 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: |
+          echo '::error::This PR is labeled as "do not merge", remove the label to make this check pass.'
+          exit 1