On Fri, 13 Nov 2009, Sven Joachim wrote: > > Done. > > It seems you have not pushed this yet. Done now (I did not check that my git push worked, and it did not, I was not up-to-date). Cheers, -- Raphaël Hertzog