On 4/10/12, Timon Gehr <timon.gehr at gmx.ch> wrote: > Yes, it is fixed in git head. Sorry for the noise. Sorry for my noise too, I didn't know it was fixed in git head. :)