Hello, 

in our org-mode generated HTML pages we find these snippets:

<script type="text/javascript">
<!--/*--><![CDATA[/*><!--*/
 function CodeHighlightOn(elem, id)
 { ...
 }
 function CodeHighlightOff(elem, id)
 { ...
 }
/*]]>*///-->
</script>

We have just noticed that MS Internet Explorer complains that these lines pose a security risk (Firefox and Safari have no problem with them), deleting the JavaScript code solves the issue. I have found a link that might explain the problem: http://www.codingforums.com/archive/index.php/t-78039.html
(the problem is limited to locally accessed HTML pages, not HTML content that is accessed over a network; we now use org-mode to generate a locally stored collection of online help files in HTML - so this is an awkward issue for us)

As our pages do not need this JavaScript code anyway, having a switch that prevents this code from being included would be a good solution from our point of view. Naturally, we could have a "postprocessing" script to remove the offending lines before releasing the HTML content, however, that seems such a crude approach.

Here is a suggestion, maybe there could be a new switch for #+OPTIONS:

javascript: turn on/off inclusion of JavaScript helper code for code highlighting

and while we are at it:

css: turn on/off inclusion of stylesheet?

Warm regards,
 Stefan
-- 
Dr. Stefan Vollmar, Dipl.-Phys.
Head of IT group
Max-Planck-Institut für neurologische Forschung
Gleuelerstr. 50, 50931 Köln, Germany
Tel.: +49-221-4726-213  FAX +49-221-4726-298
Tel.: +49-221-478-5713  Mobile: 0160-93874279
Email: vollmar@nf.mpg.de   http://www.nf.mpg.de