On Thu, Feb 23, 2012 at 10:32:42PM +0100, Johan Van de Wauw wrote: > This is fixed in the git repository now. > Missed a push round? -- Francesco P. Lovergine