edwinb/Idris-dev — pull request #302 by raichoo (2013-05-03 10:21:19+00:00)
Title: vim: remove bad whitespace highlight

should be done in individual vimrc