Closed cdepillabout closed 9 years ago
The commentstring setting is used in plugins like Tim Pope's "commentary" plugin. commentstring defaults to "/*", which is not usable by idris. This commit changes it to "--".
Thanks.
The commentstring setting is used in plugins like Tim Pope's "commentary" plugin. commentstring defaults to "/*", which is not usable by idris. This commit changes it to "--".