From da9d44df2dfec2746ee9693f71137f4c69f31306 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 12 Aug 2024 11:51:50 +0200
Subject: [PATCH] feat: handle \r on all operating systems in IO.FS.lines
 (#4973)

Closes: #4573
---
 src/Init/System/IO.lean  |  2 +-
 tests/lean/run/4573.lean | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/4573.lean

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