# HG changeset patch
# User wenzelm
# Date 1606680586 -3600
# Node ID fbee4d09a221cd92997bbab7014cc06168189459
# Parent  98ecb951d911b2c665563beef06439b0e64567dc
proper source symbols in persistent data;

diff -r 98ecb951d911 -r fbee4d09a221 src/Pure/Tools/build_job.scala
--- 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 =