src/Pure/Tools/build_job.scala
changeset 76935 da3310cc00f0
parent 76933 dd53bb198eb1
child 76936 ee785742c694
--- a/src/Pure/Tools/build_job.scala	Fri Jan 06 16:50:43 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 06 16:54:16 2023 +0100
@@ -51,7 +51,7 @@
             Document.Blobs.Item(bytes, text, chunk, changed = false)
         }
 
-      val thy_source = read_source_file(thy_file).text
+      val thy_source = read_source_file(thy_file).bytes.text
       val thy_xml = read_xml(Export.MARKUP)
       val blobs_xml =
         for (i <- (1 to blobs.length).toList)