--- a/src/Pure/Admin/build_log.scala Tue Oct 18 15:18:58 2016 +0200
+++ b/src/Pure/Admin/build_log.scala Tue Oct 18 15:31:08 2016 +0200
@@ -24,9 +24,11 @@
object Prop
{
+ val separator = '\u000b'
+
def multiple(name: String, args: List[String]): Properties.T =
if (args.isEmpty) Nil
- else List(name -> YXML.string_of_body(XML.Encode.list(XML.Encode.string)(args)))
+ else List(name -> args.mkString(separator.toString))
val build_tags = "build_tags" // multiple
val build_args = "build_args" // multiple