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

[Jonathan M Davis]

On Tuesday, October 08, 2013 01:18:45 Walter Bright 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.

That's perfectly fine as long as it's to your branch (which it normally would 
be for a PR). The problem is when it's done to master. However, I didn't know 
that you could get away with doing a push without listing the target branch. I 
always list the target branch, which is less error-prone, since you're never 
going to push -f to master.

- Jonathan M Davis