you can delete a remote branch using git push origin --delete <oldbranch>
or you can do it via the GitHub interface in Code / branches. I think if
it's deleted remotely, then your tracking branch will get removed when you
pull, unless it's ahead of the remote.
On Thu, Mar 24, 2016 at 12:53 PM, Syd Bauman
I don’t think we have a policy as yet. Some time not too long after they get merged back into dev and work on them stops. Post-release is probably a good time to clean up leftover branches, but there’s no reason to keep them past their sell-by date.
Maybe we should say the branch owner is responsible for deleting branches that have been pushed to the repo after they stop work on them?
I think that's a fine idea. Just double-checking, would we use `git branch -d OLDBRANCH` or `git branch -D OLDBRANCH`, or does it matter? (And it looks like a deletion does not require a commit message; but one would have to push after executing the -d or -D, right?) -- tei-council mailing list tei-council@lists.tei-c.org http://lists.lists.tei-c.org/mailman/listinfo/tei-council
PLEASE NOTE: postings to this list are publicly archived