[dmd-internals] Fixing github pull requests that I borked up

[Jacob Carlborg]

On Oct 08, 2013, at 10:18 AM, Walter Bright <walter at digitalmars.com> wrote:

> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.puremagic.com/pipermail/dmd-internals/attachments/20131008/b1119732/attachment.html>