idris-lang/Idris-dev — pull request #1057 by ahmadsalim (2014-04-12 14:59:47+00:00)
Title: Fix help options for ":module" and ":metavars"

Remove ":m" as a shortcut for ":module" in help as it is used for ":metavars".
Remove argument for ":metavars" as it doesn't take any.