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)