| changeset 65589 | f70c617e9c26 |
| parent 64934 | 795055a0be98 |
| child 66232 | be0ab4b94c62 |
--- 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)