--- a/src/Pure/Admin/build_log.scala Thu Jun 27 23:45:32 2024 +0200
+++ b/src/Pure/Admin/build_log.scala Thu Jun 27 23:53:31 2024 +0200
@@ -650,7 +650,7 @@
): Option[Bytes] =
if (errors.isEmpty) None
else {
- Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
+ Some(YXML.bytes_of_body(XML.Encode.list(XML.Encode.string)(errors)).
compress(cache = cache))
}
--- a/src/Pure/General/properties.scala Thu Jun 27 23:45:32 2024 +0200
+++ b/src/Pure/General/properties.scala Thu Jun 27 23:53:31 2024 +0200
@@ -45,7 +45,7 @@
def encode(ps: T): Bytes = {
if (ps.isEmpty) Bytes.empty
- else Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+ else YXML.bytes_of_body(XML.Encode.properties(ps))
}
def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
@@ -59,7 +59,7 @@
): Bytes = {
if (ps.isEmpty) Bytes.empty
else {
- Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
+ YXML.bytes_of_body(XML.Encode.list(XML.Encode.properties)(ps)).
compress(options = options, cache = cache)
}
}