[petsc-dev] git repo branches housekeeping

[Jed Brown]

"Balay, Satish via petsc-dev" <petsc-dev at mcs.anl.gov> writes:

>> Would it make sense to make this cleanup in a regular basis? Once a PR is
>> merged into master, what's the point of keeping the branch around until
>> next release? It makes it heavier to search for a branch in Bitbucket, "git
>> remote show origin" produces huge listing.
>> I try hard myself of remembering to remove my merged branches, or select
>> "close source branch" when I make the PR.
>
> Well I think the prior thought was - if some additional fixes are
> needed to that branch after merge to master - its good to keep it
> around. But I guess this use-case is rare..

Yeah, pretty rare and the branch name is mentioned in the merge commit
so it can be recreated when needed.  (Doing so is desirable because it
allows in-development branches to obtain a bug fix without possibly
unrelated features from 'master'.)