
<html dir="ltr"><head></head><body style="text-align:left; direction:ltr;"><div>Hi,</div><div><br></div><div>I didn't observe this bug anymore for some years. Hence, I close the bug.</div><div><br></div><div>Cheers,</div><div>Bruno</div></body></html>