diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 662f5ca98b..ba4ac8e298 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -496,7 +496,7 @@ partial def lines (fname : FilePath) : IO (Array String) := do pure lines else if line.back == '\n' then let line := line.dropRight 1 - let line := if System.Platform.isWindows && line.back == '\x0d' then line.dropRight 1 else line + let line := if line.back == '\r' then line.dropRight 1 else line read <| lines.push line else pure <| lines.push line diff --git a/tests/lean/run/4573.lean b/tests/lean/run/4573.lean new file mode 100644 index 0000000000..23a851482d --- /dev/null +++ b/tests/lean/run/4573.lean @@ -0,0 +1,12 @@ +def test : IO Unit := do + let tmpFile := "4573.tmp" + let baseLines := #["foo", "bar", "foobar"] + let content := baseLines[0] ++ "\r\n" ++ baseLines[1] ++ "\n" ++ baseLines[2] + IO.FS.writeFile tmpFile content + let readLines ← IO.FS.lines tmpFile + IO.println <| baseLines == readLines + IO.FS.removeFile tmpFile + +/-- info: true -/ +#guard_msgs in +#eval test