An example:

    https://github.com/D-Programming-Language/dmd/pull/2615

See all those extra commits in there? That's because I did a:

    git push -f

from the wrong branch. Git, miserable program that it is, has no:

    git undo

which it so desperately needs. Anyhow, this royally borked up github. Brad Roberts came riding the rescue, and got the damage to the main repo undone. However, the PR's did not fix themselves.

However, I discovered that if I:

    git checkout myfixbranch
    git commit --amend -a
    git push -f

for my PR's, one by one, it fixed the PR's. So I fixed mine, but y'all will likely each have to fix yours one by one. Brad has an email in to github support to see if this can be fixed without needing each of us to do it, but in the meantime, or if that doesn't pan out, this should work.

Sorry about this.
_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

On Oct 07, 2013, at 09:44 PM, Walter Bright <walter@digitalmars.com> wrote:

> An example:
>
> https://github.com/D-Programming-Language/dmd/pull/2615
>
> See all those extra commits in there? That's because I did a:
>
> git push -f

Why did you do a force push in the first place? If you can't push, you shouldn't just blindly add "-f" to force the push. You should stop and think of why you can't push it without force in the first place. You need to stop doing this. No offense, but you obviously can not completely handle git. Either learn how to handle it or ask some one, BEFORE you're doing something like this.

> from the wrong branch. Git, miserable program that it is, has no:
>
> git undo
>
> which it so desperately needs. Anyhow, this royally borked up github. Brad Roberts came riding the rescue, and got the damage to the main repo undone. However, the PR's did not fix themselves.

I don't know what exactly had happened or how Brad "fixed" this, but I'm pretty sure it's possible to correctly fix this without breaking the pull requests. Just reset back the history to the sate it was before the force push. Since you already made a push force, another push force is needed to fix the problem. Then correctly make the changes you wanted to make.

--
/Jacob Carlborg

On 10/8/2013 12:06 AM, Jacob Carlborg wrote:
> On Oct 07, 2013, at 09:44 PM, Walter Bright <walter@digitalmars.com> wrote:
>
>> An example:
>>
>> https://github.com/D-Programming-Language/dmd/pull/2615
>>
>> See all those extra commits in there? That's because I did a:
>>
>> git push -f
>
> Why did you do a force push in the first place? If you can't push, you shouldn't just blindly add "-f" to force the push. You should stop and think of why you can't push it without force in the first place. You need to stop doing this. No offense, but you obviously can not completely handle git. Either learn how to handle it or ask some one, BEFORE you're doing something like this.

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.

>
>> from the wrong branch. Git, miserable program that it is, has no:
>>
>> git undo
>>
>> which it so desperately needs. Anyhow, this royally borked up github. Brad
>> Roberts came riding the rescue, and got the damage to the main repo undone.
>> However, the PR's did not fix themselves.
>
> I don't know what exactly had happened or how Brad "fixed" this, but I'm pretty sure it's possible to correctly fix this without breaking the pull requests. Just reset back the history to the sate it was before the force push. Since you already made a push force, another push force is needed to fix the problem. Then correctly make the changes you wanted to make.

Brad used a git reset followed by a git push with -f. The github master is now correct, but it's a mystery why the PR's are messed up.

_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

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
_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

On 10/8/13 12:06 AM, Jacob Carlborg wrote:
> On Oct 07, 2013, at 09:44 PM, Walter Bright <walter@digitalmars.com> wrote:
>
>> An example:
>>
>> https://github.com/D-Programming-Language/dmd/pull/2615
>>
>> See all those extra commits in there? That's because I did a:
>>
>> git push -f
>
> Why did you do a force push in the first place? If you can't push, you shouldn't just blindly add
> "-f" to force the push. You should stop and think of why you can't push it without force in the
> first place. You need to stop doing this. No offense, but you obviously can not completely handle
> git. Either learn how to handle it or ask some one, BEFORE you're doing something like this.

Completely agreed.

>> from the wrong branch. Git, miserable program that it is, has no:
>>
>> git undo
>>
>> which it so desperately needs. Anyhow, this royally borked up github. Brad
>> Roberts came riding the rescue, and got the damage to the main repo undone.
>> However, the PR's did not fix themselves.
>
> I don't know what exactly had happened or how Brad "fixed" this, but I'm pretty sure it's possible
> to correctly fix this without breaking the pull requests. Just reset back the history to the sate it
> was before the force push. Since you already made a push force, another push force is needed to fix
> the problem. Then correctly make the changes you wanted to make.

The fix was merely repushing the commit id of the previously head of master back as the current head of master.  Something internal to github's management of pulls got confused at that point.  So far, no response to my support request.

_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

On 10/8/2013 1:25 AM, Jonathan M Davis wrote:
> 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.

I'm not really sure why that one time I did it it applied it to master rather than the branch. Anyhow, what is the syntax to apply it only to a branch?
_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

On Tuesday, October 08, 2013 01:56:21 Walter Bright wrote:
> On 10/8/2013 1:25 AM, Jonathan M Davis wrote:
> > 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.
> 
> I'm not really sure why that one time I did it it applied it to master rather than the branch. Anyhow, what is the syntax to apply it only to a branch?

Assuming that your github repo is named origin (which is normally the case), it should be

git push origin branch-name

or for forcing it,

git push -f origin branch-name

and git will complain if you try and push it to a branch that doesn't have the same name as your local one. So, it should catch any mismatch. And the only reason that you'd risk pushing to the main repo that way is if you accidentally typed upstream instead of origin, and you'd have to combine both upstream and master to actually mess with master on the main repo (and since pull requests really should be coming from branches, not master, the odds of accidentally pushing to master on upstream should be quite low).

If you have to actually push to the main repo, then presumably it would be

git push upstream branch-name

or

git push -f upstream branch-name

though I'd generally expect you to only be pushing to upstream when creating branches for releases and whatnot, not pull requests (I'm not sure that you even _can_ create pull requests to the main repo from branches on the main repo).

- Jonathan M Davis
_______________________________________________
dmd-internals mailing list
dmd-internals@puremagic.com
http://lists.puremagic.com/mailman/listinfo/dmd-internals

On Oct 08, 2013, at 10:18 AM, Walter Bright <walter@digitalmars.com> 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.

I'm not sure how your workflow is but if you need to amend a pull request I would think you would do something like this:

1. Merge the pull request on your local machine
2. Make your changes and amend
3. Push to your own fork at Github (origin) or push to upstream if the pull request should be merged into master. No need to use "push -f"

> Brad used a git reset followed by a git push with -f. The github master is now correct, but it's a mystery why the PR's are messed up.

I've learned that what's show in pull requests on Github is not always 100% accurate. I would suggest merging a pull request on a local machine and see what changes it actually contains.

--
/Jacob Carlborg

On Oct 08, 2013, at 10:26 AM, Brad Roberts <braddr@puremagic.com> wrote:

> The fix was merely repushing the commit id of the previously head of master back as the current head of master. Something internal to github's management of pulls got confused at that point. So far, no response to my support request.

As I replied to Walter:

I've learned that what's show in pull requests on Github is not always 100% accurate. I would suggest merging a pull request on a local machine and see what changes it actually contains.

--
/Jacob Carlborg

On Oct 08, 2013, at 10:25 AM, Jonathan M Davis <jmdavisProg@gmx.com> wrote:

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

It depends on your git settings. You can tell git to either push all your branches (that have a matching branch on the remote) when doing "git push" or just push the active branch. There are couple more alternatives as well.

See the first four examples here:

https://www.kernel.org/pub/software/scm/git/docs/git-push.html#_examples

Have a look at this as well:

https://www.kernel.org/pub/software/scm/git/docs/git-config.html

Search for "push.default". The default value of this setting was/will be changed in Git 2.0.

--
/Jacob Carlborg