idris-lang/Idris-dev — pull request #1414 by Heather (2014-07-22 12:22:21+00:00)
Title: rename writeLine to writeString, add writeLine

Since WriteLine doesn't add line ending for now