[petsc-dev] git repo branches housekeeping

[Smith, Barry F.]

> On Apr 1, 2019, at 10:37 AM, Balay, Satish via petsc-dev <petsc-dev at mcs.anl.gov> wrote:
> 
> On Mon, 1 Apr 2019, Lisandro Dalcin wrote:
> 
>> On Fri, 29 Mar 2019 at 19:22, Balay, Satish via petsc-dev <
>> petsc-dev at mcs.anl.gov> wrote:
>> 
>>> ref: https://lists.mcs.anl.gov/pipermail/petsc-dev/2018-April/022748.html
>>> 
>>> I've deleted all development branches that are already merged into
>>> maint (v3.11) from https://bitbucket.org/petsc/petsc
>>> 
>>> 
>> 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..
> 
> Also - this cleanup can be done perhaps easily on the server [by
> someone who can check on it regularly - as doing this when closing PR
> cannot be automated] - but folk would have to do this on their clones
> too [as cleanup on the server does not automatically do cleanup in
> clones].

   This is, IMHO, a weakness of git. It is crazy to impose this type of housekeeping directly on all 1000 users of a repository. 

  Barry

> Satish