[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