Martin Pitt [2019-10-23 7:53 +0200]:
After a PR of mine lands, I always manually press the "Delete
branch" button,
so that "git branch -al" does not pile up cruft and remains an useful tool. I
guess/hope that most other people do the same?
GitHub recently added a simple config option to automate that:
https://help.github.com/en/github/administering-a-repository/managing-the...
I should clarify this a little bit: This means that the merged branch on the
github remote will automatically be cleaned. It will of course still exist on
your local checkout. You can do "git remote prune <yourorigin>" to
locally
clean up the ones that got removed remotely.
Also, at least the "Delete branch" button in merged PRs has an undo button,
just in case. I'd think that the automatic deletion would have that as well.
Martin