[racket-dev] Sorry.

40 minutes ago, Jens Axel Søgaard wrote:
> 
> I made a mistake pushing some commits.
> Rather than mess things more up, I hope
> some one has enough git-fu to undo the commit.

I think that I reverted the whole push now, and made it go back to
where it was before it -- 055512b4e8.

This was a non-fast-forward push, so:

* If you have not updated your repository between the time of the push
  and just now, then things should look fine.  That's assuming that my
  push was a clean reversal of the broken push -- so if you do see
  problems then let me know.

* If you *have* updated your repository between the two times, then
  you're now in a bad state, where the server had changed its history
  which contradicts your own history.  I'm optimistically assuming
  that nobody had that update -- but if you did, then please let me
  know soon.  (I'll probably be away from my computer in about 15
  minutes though, so if you're in such a situation and you don't tell
  me about it now, then send me a phone number that I can call later
  on, or just wait until I'm on-line again.)

* Jens: as for the push itself, since I reverted the whole thing, it
  needs to be done again -- my guess is that the best way to approach
  it (given that your repo is most likely in a broken state now) is to
  just get whatever is on the server as is so you're in a clean state,
  then apply the patch that was part of the broken push (the part that
  is below the "Overall Diff" header).


> Normally push refused to do anything but fast-forward
> commits, but the commit looks wrong on Github.

Can you check that it looks fine on GH now?

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!