idris-lang/Idris-dev — pull request #1570 by jfdm (2014-10-02 21:25:08+00:00)
Title: Removed dead commented out code.

The actual commit was to lines 701--716. The other changes were from editor deleting trailing whitespace from the code.