ci: prevent merge of PRs with do-not-merge label

Co-authored-by: Paul Meyer <[email protected]>
edgelesssys · Nov 18, 2024 · 18923b5 · 18923b5
1 parent 3a82af8
commit 18923b5
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/.github/workflows/require_label.yml b/.github/workflows/require_label.yml
@@ -22,3 +22,14 @@ 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 -n "::error "
+          tee "${GITHUB_STEP_SUMMARY}" <<'EOF'
+          This PR is labeled as `do not merge`, remove the label to make this check pass.
+          EOF
+          exit 1