idris-hackers/idris-mode — pull request #147 by david-christiansen (2014-05-19 15:04:19+00:00)
Title: Add command and menu item to specify packages

This is less than perfect, because it lets some junk through, but it's
better than nothing.