idris-lang/Idris-dev — pull request #905 by david-christiansen (2014-02-16 18:04:03+00:00)
Title: Actually parse documentation strings

This patch does the following:
* The parser no longer ignores documentation comments
* Two invalid documentation comments in the stdlib are converted to normal comments
* Documentation comments can span multiple lines when defined with `--`. The lines are concatenated.