Commits


Github: add mechanism to autoclose prs The GitHub repository is read-only and exists so that CI can be run. We do not want PRs to be issued against the repository, so should someone do that, the PR is closed with a friendly message pointing them to the mailing list instead.