From 08474e04ff49b28798d61a8710e66ed74eb4b70b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 5 Jul 2018 16:47:53 +0200
Subject: [PATCH] fix(library/system/io): read_to_end: work around UTF-8 bug in
 `io.read`

---
 library/system/io.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/system/io.lean b/library/system/io.lean
index b192f2c99b..d8b1774c90 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -142,7 +142,8 @@ iterate "" $ λ r,
     if done
     then return none
     else do
-      c ← read h 1024,
+      -- HACK: use less efficient `get_line` while `read` is broken
+      c ← get_line h,
       return $ some (r ++ c)
 
 def read_file (fname : string) (bin := ff) : io string :=