idris-hackers/idris-mode — pull request #99 by david-christiansen (2014-03-18 15:39:03+00:00)
Title: Add a note about fonts and colors to the readme

There are instructions for changing them. Fixes #92.