On Oct 07, 2016, at 01:35 PM, Oleg Broytman wrote: > $ git fetch github pull/$ID/head:$BRANCHNAME > $ git checkout master > $ git merge --squash $BRANCHNAME > $ git branch -d $BRANCHNAME
This works well, and is generally the instructions that GitLab provides for
local CLI merges. A few things to note.
> $ git fetch github pull/$ID/head:$BRANCHNAME
^^^^^^
This is the remote name, so it will usually be 'origin' but it can be anything
(i.e. it's up to the local user).
> $ git fetch github pull/$ID/head:$BRANCHNAME
^^^^^^^^^^^^
This isn't strictly necessary. If not given, use FETCH_HEAD. And if you want
to do some things with the branch before you merge it to master (e.g. add
NEWS, uncommit code changes to make sure that the tests prove a fix works,
etc.) then you can:
$ git co -b $BRANCHNAME FETCH_HEAD
Of course, $BRANCHNAME can be anything you want.
Cheers,
-Barry
pgp5qCk05d5uI.pgp
Description: OpenPGP digital signature
_______________________________________________ core-workflow mailing list core-workflow@python.org https://mail.python.org/mailman/listinfo/core-workflow This list is governed by the PSF Code of Conduct: https://www.python.org/psf/codeofconduct
