On 4/10/12, Timon Gehr <[email protected]> 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. :)

Reply via email to