diff -r fffb978dd683 -r da3310cc00f0 src/Pure/Tools/build_job.scala --- 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)