src/Pure/Tools/dump.scala
changeset 80437 2c07b9b2f9f4
parent 80425 efa212a6699a
child 80489 e0568c7b5bed
--- a/src/Pure/Tools/dump.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -33,7 +33,7 @@
       write(file_name, Bytes(text))
 
     def write(file_name: Path, body: XML.Body): Unit =
-      write(file_name, Symbol.encode(YXML.string_of_body(body)))
+      write(file_name, YXML.bytes_of_body(body, recode = Symbol.encode))
   }
 
   sealed case class Aspect(