changeset 72962 | af2d0e07493b |
parent 72946 | 9329abcdd651 |
child 73031 | f93f0597f4fb |
--- a/src/Pure/PIDE/command.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/PIDE/command.scala Sun Dec 20 15:47:54 2020 +0100 @@ -30,7 +30,7 @@ src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) { - def read_file: String = File.read(name.path) + def read_file: Bytes = Bytes.read(name.path) def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node)