python
Enable auto-delete of merged branches on https://github.com/python/devguide/
The short story
It would be nice if branches were auto-deleted after a PR is merged.
Long version
You can have head branches automatically deleted after pull requests are merged in your repository.
https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-the-automatic-deletion-of-branches is the relevant documentation. https://github.blog/changelog/2019-07-31-automatically-delete-head-branches-of-pull-requests/ is the relevant changelog entry.
Does this affect only upstream branches, or delete user branches too? The former doesn't really do anything now that we've enabled branch protection to prevent that, while the later seems a little intrusive (especially for squash-merges, where the original commits are lost) and something that should be up to the user managing their fork, not the upstream repository, since it has no effect on the latter (unless I'm understanding something wrong). For that I greatly prefer the GitHub Refined auto-delete feature instead, which each user can control individually to their own preference.
Before you enable this I may need to make changes to miss-islington. It has logic for deleting branch.
