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

[Jacob Carlborg]

On 8 okt 2013, at 21:00, Jonathan M Davis <jmdavisProg at gmx.com> wrote:

> 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.


I don't see why amending a pull request requires push -f. I mean, he won't have access to the repository where the pull request originated from. So he can only chose to push to upstream or he's own repository. In both of these cases he doesn't need push -f. Unless he merged the pull request via Github.

Or he's amending his own pull request. I didn't think of that. Then push -f will be necessary.

-- 
/Jacob Carlborg