Provide a bot to close GitHub PRs of read-only mirrors
Since GitHub seems to be unable to provide a way to disable Pull Requests for repositories we might want to deploy a script to automatically close PRs with a message pointing to the GitLab repository.
The Linux repo uses this python script, it does what we want and is quite battle proven. However, it polls the GitHub API instead of providing a web hook endpoint, which might introduce unnecessary overhead.
This project uses web hooks, but it only acts on merged PRs.
Also, where should we deploy the script and optionally the web hook endpoint? Directly on the GitLab server?