On Oct 08, 2013, at 10:18 AM, Walter Bright <[email protected]> wrote:
I'm not sure how your workflow is but if you need to amend a pull request I would think you would do something like this:
1. Merge the pull request on your local machine
2. Make your changes and amend
3. Push to your own fork at Github (origin) or push to upstream if the pull request should be merged into master. No need to use "push -f"
I've learned that what's show in pull requests on Github is not always 100% accurate. I would suggest merging a pull request on a local machine and see what changes it actually contains.
--
/Jacob Carlborg
Because I often need to amend a pull request, and I was told it was done with:
git --amend -a
git push -f
and I've been doing that successfully since I've been doing PR's.
I'm not sure how your workflow is but if you need to amend a pull request I would think you would do something like this:
1. Merge the pull request on your local machine
2. Make your changes and amend
3. Push to your own fork at Github (origin) or push to upstream if the pull request should be merged into master. No need to use "push -f"
Brad used a git reset followed by a git push with -f. The github master is now
correct, but it's a mystery why the PR's are messed up.
I've learned that what's show in pull requests on Github is not always 100% accurate. I would suggest merging a pull request on a local machine and see what changes it actually contains.
--
/Jacob Carlborg
_______________________________________________ dmd-internals mailing list [email protected] http://lists.puremagic.com/mailman/listinfo/dmd-internals
