search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Make System.File.readFile keep newlines #332

Closed ziman closed 4 years ago

ziman commented 4 years ago

System.File.readFile on a file containing "foo\nbar" returns "foobar".

This patch fixes it. I'm not sure about the efficiency but I hope it's not horrible.

edwinb commented 4 years ago

Oh, I fixed this without noticing this PR, sorry! I did it the same way. There's still something not quite right, because if there isn't a newline at the end of the file it shouldn't be in the input that's read. But this at least restores the old behaviour.