[petsc-dev] git repo branches housekeeping

Balay, Satish balay at mcs.anl.gov
Mon Apr 1 13:54:11 CDT 2019


On Mon, 1 Apr 2019, Jed Brown wrote:

> "Balay, Satish" <balay at mcs.anl.gov> writes:
> 
> > On Mon, 1 Apr 2019, Jed Brown via petsc-dev wrote:
> >
> >> "Smith, Barry F. via petsc-dev" <petsc-dev at mcs.anl.gov> writes:
> >> 
> >> >    This is, IMHO, a weakness of git. It is crazy to impose this type of housekeeping directly on all 1000 users of a repository. 
> >> 
> >> Perhaps this should be the default:
> >> 
> >>   git config --global fetch.prune true
> >
> > or use 'git fetch -p' [ mentioned in my instructions]. I prefer
> > 'fetch' to 'pull' anyway [as it keeps my git prompt sane] - so this
> > works out well for me.
> >
> >> 
> >> But, it would make it harder to recover if someone accidentally deletes
> >> a branch on the server.
> >> 
> >>   https://stackoverflow.com/a/40842589/33208
> >
> > This updates the origin/* references to remote branches - but does not
> > delete locally checked out branches [if any] - they have to be
> > manually deleted [as mentioned in my instructions]
> 
> Yes, but those are branches that a person has directly interacted with.
> The many other branches would be quietly pruned.

Agree..

We could do:

- try to close as many branches as possible on the server [with each PR].
- recommend folks use  'git config --global fetch.prune true' or 'git fetch -p' in their regular workflow.
- folks could do housekeeping on their clones (aka delete local branches) at their own convenient schedule.
- and I'll continue to send the 'housekeeping' e-mail reminder after release.

Satish


More information about the petsc-dev mailing list