idris-lang/Idris-dev — pull request #701 by jfdm (2013-12-05 09:17:45+00:00)
Title: Added inputIdrisListing command to load external files.

Improvements to idrislang.sty