Add a bot to close PRs automatically

leanprover · Jan 3, 2024 · 55ed864 · 55ed864
1 parent 0152f5d
commit 55ed864
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/.github/workflows/close-pr.yml b/.github/workflows/close-pr.yml
@@ -0,0 +1,14 @@
+name: Close Pull Request
+
+on:
+  pull_request_target:
+    types: [opened]
+
+jobs:
+  run:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: superbrothers/close-pull-request@v3
+      with:
+        # Optional. Post a issue comment just before closing a pull request.
+        comment: "This repository does not accept pull requests. Please open an issue describing the changes that you'd like to see in the book."