idris-lang/Idris-dev — pull request #545 by david-christiansen (2013-10-18 09:45:24+00:00)
Title: Check for file extension in :e

Now, when Idris is invoked without a module file extension, :e will add it.

Fixes #526.