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] Satish