Can we make it so that these pre-commit branches are deleted upon merging (but not repo-wide)? Otherwise, we have to remember to delete them ourselves when we merge.
This looks, fiddly to do for a single type of PR, e.g the docs only talk about deleting them all.
One route might be to get this into a Github action, but I would probably be in favour of the maintainers (read me) being more careful and deleting when we merge.
updates: