"Smith, Barry F. via petsc-dev" <[email protected]> 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
