author | wenzelm |
Sun, 29 Nov 2020 21:09:46 +0100 | |
changeset 72783 | fbee4d09a221 |
parent 72782 | 98ecb951d911 |
child 72784 | ed75dde8061a |
--- a/src/Pure/Tools/build_job.scala Sun Nov 29 17:57:20 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Sun Nov 29 21:09:46 2020 +0100 @@ -170,7 +170,7 @@ { val theory_name = snapshot.node_name.theory val args = Protocol.Export.Args(theory_name = theory_name, name = name) - val bytes = Bytes(YXML.string_of_body(xml)) + val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) if (!bytes.is_empty) export_consumer(session_name, args, bytes) } def export_text(name: String, text: String): Unit =