[petsc-dev] git repo branches housekeeping

[Jed Brown]

"Balay, Satish" <balay at mcs.anl.gov> writes:

> On Mon, 1 Apr 2019, Jed Brown via petsc-dev wrote:
>
>> "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
>
> 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.