> On 1 Apr 2019, at 20:54, Balay, Satish via petsc-dev <[email protected]>
> wrote:
>
> On Mon, 1 Apr 2019, Jed Brown wrote:
>
>> "Balay, Satish" <[email protected]> writes:
>>
>>> On Mon, 1 Apr 2019, Jed Brown via petsc-dev wrote:
>>>
>>>> "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
>>>
>>> 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
