idris-lang/Idris-dev — pull request #874 by puffnfresh (2014-02-10 16:25:48+00:00)
Title: Execute JavaScript output after DOMContentLoaded

Previously, JavaScript generated for the browser would only execute on
the DOMContentLoaded event. We should also check if the browser is
already ready. We can do this with the following:

document.readyState == "complete" || document.readyState == "loaded"

Requesting review from the great @raichoo :racehorse: