idris-hackers/idris-mode — pull request #197 by david-christiansen (2014-06-19 15:56:41+00:00)
Title: Move keybinding hooks to new file

Fixes #195