[petsc-dev] git repo branches housekeeping

Jed Brown jed at jedbrown.org
Mon Apr 1 10:54:15 CDT 2019

"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.


More information about the petsc-dev mailing list