1 /* This is used in bin/mozilla/kopf.pl to switch the HTML sidemenu on/off
2 2010, Sven Donath, lxo@dexo.de */
6 function Switch_Menu(framesize)
11 parent.document.getElementById('menuframe').setAttribute('cols','30,*')
16 framesize = framesize + ',*';
17 parent.document.getElementById('menuframe').setAttribute('cols',framesize);