HTMLDocument undefined

[texcoffier]

For some Internet Explorer version HTMLDocument is undefined.

In pythonjs/runtime/pythonpythonjs.py the following code should be added:

if not __NODEJS__ and not __WEBWORKER__:
        if typeof(HTMLDocument) == 'undefined':
                HTMLDocument = Document