On Mon, 1 Apr 2019, Jed Brown wrote: > "Balay, Satish" <ba...@mcs.anl.gov> writes: > > > On Mon, 1 Apr 2019, Jed Brown via petsc-dev wrote: > > > >> "Smith, Barry F. via petsc-dev" <petsc-dev@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