[petsc-dev] git repo branches housekeeping

[Balay, Satish]

On Mon, 1 Apr 2019, Hapla  Vaclav wrote:

> > - 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?

Or the person merging the PR would use the web interface to do this
merge - and 'tick the checkbox' at that merge step.

And I would scan branches weekly or [whenever I remember] to spot
merged branches that were not deleted.

Note: When a PR is from a fork - we manually create a local branch to
track its progress through next. Such branches would have to be
manually deleted.

Satish