Auto-close PRs on the GitHub mirror

Bug: none
Change-Id: I876783bd040c5cc845427a4530e9feb3773c8bf7
Reviewed-on: https://chromium-review.googlesource.com/c/devtools/devtools-frontend/+/6695694
Reviewed-by: Benedikt Meurer <[email protected]>
Commit-Queue: Benedikt Meurer <[email protected]>
Auto-Submit: Alex Rudenko <[email protected]>
Commit-Queue: Alex Rudenko <[email protected]>

Author: OrKoN

.github/workflows/auto-close-prs.yml

@@ -0,0 +1,15 @@
+name: Auto-close PRs
+
+on:
+  pull_request:
+    types: [opened]
+
+jobs:
+  auto-close:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Close Pull
+        # See https://cli.github.com/manual/gh_pr_close
+        run: gh pr close --comment "Auto-closing the pull request because we do not accept PRs via the GitHub mirror. See README.md on how to contribute to DevTools." --delete-branch "1"
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}