From 670291480181701d99e1d1d3d83f162e2e5e8fa3 Mon Sep 17 00:00:00 2001
From: Hugo van Kemenade <hugovk@users.noreply.github.com>
Date: Wed, 19 Apr 2023 20:35:00 -0600
Subject: [PATCH] CI: Do not allow merge if labelled DO-NOT-MERGE

---
 .github/workflows/require-pr-label.yml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 .github/workflows/require-pr-label.yml

diff --git a/.github/workflows/require-pr-label.yml b/.github/workflows/require-pr-label.yml
new file mode 100644
index 00000000000000..151a60c2c04d26
--- /dev/null
+++ b/.github/workflows/require-pr-label.yml
@@ -0,0 +1,18 @@
+name: Check labels
+
+on:
+  pull_request:
+    types: [opened, reopened, labeled, unlabeled, synchronize]
+
+jobs:
+  label:
+    name: DO-NOT-MERGE
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+
+    steps:
+      - uses: mheap/github-action-required-labels@v4
+        with:
+          mode: exactly
+          count: 0
+          labels: "DO-NOT-MERGE"