changeset 80480 | 972f7a4cdc0e |
parent 79844 | ac40138234ce |
child 80510 | bbeb2f2049aa |
--- a/src/Pure/Tools/server.scala Tue Jul 02 22:38:00 2024 +0200 +++ b/src/Pure/Tools/server.scala Tue Jul 02 23:13:35 2024 +0200 @@ -46,7 +46,7 @@ def parse(argument: String): Any = if (argument == "") () - else if (YXML.detect_elem(argument)) YXML.parse_elem(argument) + else if (YXML.detect_elem(argument)) YXML.parse_elem(YXML.Source(argument)) else JSON.parse(argument, strict = false) def unapply(argument: String): Option[Any] =