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

Jacob Carlborg doob at me.com
Tue Oct 8 12:46:21 PDT 2013


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



More information about the dmd-internals mailing list