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

Brad Roberts braddr at puremagic.com
Tue Oct 8 13:49:37 PDT 2013


On 10/8/13 12:46 PM, Jacob Carlborg wrote:
> 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.
>

An amend is a history rewrite, even if a small one.  If the amended commit ever made it out of his 
tree into github, a -f is necessary.


More information about the dmd-internals mailing list