[petsc-dev] git repo branches housekeeping

[Jed Brown]

"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

But, it would make it harder to recover if someone accidentally deletes
a branch on the server.

  https://stackoverflow.com/a/40842589/33208