src/Pure/PIDE/command.scala
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)