On 10/8/13 12:46 PM, Jacob Carlborg wrote:
On 8 okt 2013, at 21:00, Jonathan M Davis <[email protected]> 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.
_______________________________________________
dmd-internals mailing list
[email protected]
http://lists.puremagic.com/mailman/listinfo/dmd-internals
