author | wenzelm |
Wed, 05 Oct 2016 13:56:19 +0200 | |
changeset 64053 | 7ece2e14fd6c |
parent 64052 | 72fa79eab7f6 |
child 64054 | 1fc9ab31720d |
--- a/src/Pure/Tools/build_log.scala Wed Oct 05 13:27:25 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Wed Oct 05 13:56:19 2016 +0200 @@ -13,6 +13,7 @@ object Props { + def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props)) def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text)) def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =