Hello again,
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...
Does anyone object if I enable that for our cockpit projects?
I enabled this now. It says you can undelete your merged branch manually (just
like with the button).
Please yell if this gets in the way, it's easy enough to revert.
Thanks,
Martin