<font face="arial, helvetica, sans-serif">Fixed in rev 4273 -- thanks for the detailed and reproducible bug report!</font><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">J.J.</font></div>