# HG changeset patch
# User wenzelm
# Date 1476797468 -7200
# Node ID 605351c7ef970a4bd8c0b05699cdb7092da7f934
# Parent  6de1aad1e70d81315ea6be48801b9725bf39301d
another attempt to squeeze a list into a property list entry;

diff -r 6de1aad1e70d -r 605351c7ef97 src/Pure/Admin/build_log.scala
--- 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