[petsc-dev] git repo branches housekeeping

[Hapla Vaclav]

> On 1 Apr 2019, at 20:54, Balay, Satish via petsc-dev <petsc-dev at mcs.anl.gov> wrote:
> 
> On Mon, 1 Apr 2019, Jed Brown wrote:
> 
>> "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.
> 
> Agree..
> 
> We could do:
> 
> - try to close as many branches as possible on the server [with each PR].

Do you mean to tick the checkbox
  Close <branch> after the pull request is merged
when creating a PR?

Thanks,
Vaclav

> - recommend folks use  'git config --global fetch.prune true' or 'git fetch -p' in their regular workflow.
> - folks could do housekeeping on their clones (aka delete local branches) at their own convenient schedule.
> - and I'll continue to send the 'housekeeping' e-mail reminder after release.
> 
> Satish