Re: [tei-council] Fwd: shivering ...

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?)