# HG changeset patch
# User wenzelm
# Date 1493215985 -7200
# Node ID f70c617e9c265aa96f6ab8183143a4548135e2d1
# Parent  b0d8d97198b3a75b533732df9c1d2193d8d325e0
more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;

diff -r b0d8d97198b3 -r f70c617e9c26 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Apr 26 15:55:40 2017 +0200
+++ b/src/Pure/General/file.scala	Wed Apr 26 16:13:05 2017 +0200
@@ -154,7 +154,7 @@
 
   /* read */
 
-  def read(file: JFile): String = Bytes.read(file).toString
+  def read(file: JFile): String = Bytes.read(file).text
   def read(path: Path): String = read(path.file)