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(