On Fri, Sep 24, 2010 at 15:40, Guillaume Lelarge <guillaume@lelarge.info> wrote:
> Le 23/09/2010 22:47, Magnus Hagander a écrit :
>> On Thu, Sep 23, 2010 at 22:20, Guillaume Lelarge <guillaume@lelarge.info> wrote:
>>> Le 23/09/2010 22:12, git@pgadmin.org a écrit :
>> [...]
>>> the repo. I just pushed a branch there. I deleted it, so I don't think
>>> it's really that bad. Magnus, any idea on this? a "git push origin
>>> :mybugfixwork" should be enough, right? /me hopes no one had the time to
>>> grab it.
>>
>> Yeah, that should be enough. If somebody has cloned it meanwhile,
>> they'll just have to undo it themselves. For example, I just removed
>> it from the github mirror ;)
>>
>
> It's still there on github. How did you remove it?
It's not. It's cached on the web there somehow, but it's not in the
git repo. At least it wasn't last night (not in a position to check
right now).
I just pushed it with ":" at the start to the repo.
--
Magnus Hagander
Me: http://www.hagander.net/
Work: http://www.redpill-linpro.com/