On Jul 16, 2013, at 09:31 AM, Benjamin Peterson wrote: >Oops, the bad one is actually > >8889c9b5dd3a Uh, then how do we unstrip the other one? Or should we just re-clone and ignore this ever happened? ;) -Barry