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

[Jonathan M Davis]

On Tuesday, October 08, 2013 11:35:37 Jacob Carlborg wrote:
> 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"

You need push -f if you rebased. Otherwise, you shouldn't need it. Certainly, 
you shouldn't be using -f unless you actually need to, otherwise you risk 
forcing pushes that you don't actually want to succeed.

- Jonathan M Davis