Dne 12. 08. 19 v 15:42 Stefan Hundhammer napsal(a):
- After the PR is merged, simply click on the "delete branch" link that GitHub offers
you. Once it's merged, there is no need to keep it around; and it will stay around in
your local checkout anyway until you do
git fetch --prune
or
git remote prune myrepo
BTW GitHub still keeps the deleted branches internally, if needed you can just
press
the "Restore branch" button in the pull request to get it back. Or you can get
the
patch by adding the ".patch" suffix to the Pull request URL and apply it
manually
using "git apply" to a different branch.
--
Ladislav Slezák
YaST Developer
SUSE LINUX, s.r.o.
Corso IIa
Křižíkova 148/34
18600 Praha 8
--
To unsubscribe, e-mail: [email protected]
To contact the owner, e-mail: [email protected]
