10 Jul
2020
10 Jul
'20
10:03 a.m.
On 7/9/2020 3:24 PM, Mariatta wrote:
is it closed automatically ?
What is "it"? The PR itself? yes the PR becomes closed if it is merged.
The branch in your github fork is not automatically deleted. There is a button on the PR to do so. I don't know if the devguide mentions this.
The branch on your local repository is not automatically deleted when the branch on your fork is deleted. I try to remember to do it manually after hitting the button. I occassionally look through the fork branches for those that are obsolete.