[petsc-dev] git repo branches housekeeping

Balay, Satish balay at mcs.anl.gov
Mon Apr 1 15:06:54 CDT 2019

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.


More information about the petsc-dev mailing list