[plt-dev] Re: [plt] Push #20278: master branch updated

From: Jay McCarthy (jay.mccarthy at gmail.com)
Date: Fri May 21 10:39:02 EDT 2010

I thought it would do that to. Apparently the right thing to do is
"git checkout deleted-file"


On Fri, May 21, 2010 at 8:31 AM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> From what Matthias just told me, he thought he could revert a file by
> deleting it and running 'git pull'; the equivalent works in svn.  It
> didn't work, and he ran 'git commit -a' and 'git push' without
> checking 'git status' to see what state he was actually
> committing/pushing.
> Hint, hint, Matthias.  ;p
> Carl Eastlund
> On Fri, May 21, 2010 at 10:02 AM, Jay McCarthy <jay.mccarthy at gmail.com> wrote:
>> I'm curious how it actually happened.
>> On Fri, May 21, 2010 at 8:00 AM, Carl Eastlund <cce at ccs.neu.edu> wrote:
>>> On Thu, May 20, 2010 at 1:30 PM, Matthias Felleisen
>>> <matthias at ccs.neu.edu> wrote:
>>>> FUZZZ! How do I get list.rkt back? Stupid git, I want svn back.
>>> Matthew already fixed it, but... was this really a git problem, or
>>> just a "<user> has not learned git thoroughly yet" problem?  Because
>>> those were inevitable.  Granted, we're getting a lot more than the cvs
>>> -> svn switch, because svn was designed as a drop-in cvs replacement,
>>> but git was not designed as a drop-in svn replacement.
>>> --Carl

Jay McCarthy <jay at cs.byu.edu>
Assistant Professor / Brigham Young University

"The glory of God is Intelligence" - D&C 93

Posted on the dev mailing list.