Our excellent user Samuele Papa found out the code (I can&#39;t imagine where...). So we could write a small gadget as a temporary patch. I find much easier to write a simple js patch than to post a bug into bugzilla. :-) <div>
<br></div><div>Anyway: thanks. </div><div><br></div><div>Alex</div>