# HG changeset patch
# User wenzelm
# Date 1476793971 -7200
# Node ID 3073688abbe9c22aad31f3e74a49f1433efdd159
# Parent  4f11063c6e555492ba9f440f31915b1c51143d19
clarified multiple props: result needs to fit on a single line within the log file;

diff -r 4f11063c6e55 -r 3073688abbe9 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 18 13:56:49 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 14:32:51 2016 +0200
@@ -202,8 +202,8 @@
       /* output log */
 
       val meta_info =
-        Build_Log.Prop.lines(Build_Log.Prop.build_tags, build_tags) :::
-        Build_Log.Prop.lines(Build_Log.Prop.build_args, build_args) :::
+        Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
+        Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args) :::
         List(
           Build_Log.Prop.build_group_id -> build_group_id,
           Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
diff -r 4f11063c6e55 -r 3073688abbe9 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Oct 18 13:56:49 2016 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 14:32:51 2016 +0200
@@ -24,11 +24,12 @@
 
   object Prop
   {
-    def lines(name: String, lines: List[String]): Properties.T =
-      if (lines.isEmpty) Nil else List(name -> cat_lines(lines))
+    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)))
 
-    val build_tags = "build_tags"  // lines
-    val build_args = "build_args"  // lines
+    val build_tags = "build_tags"  // multiple
+    val build_args = "build_args"  // multiple
     val build_group_id = "build_group_id"
     val build_id = "build_id"
     val build_engine = "build_engine"