diff -r 69f6895dd7d4 -r 2915740fce1f src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sat Dec 31 15:32:12 2022 +0100 +++ b/src/Pure/Tools/build_job.scala Sat Dec 31 15:42:13 2022 +0100 @@ -22,7 +22,7 @@ def read_xml(name: String): XML.Body = YXML.parse_body( - Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), + Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)), cache = theory_context.cache) for {