# HG changeset patch
# User wenzelm
# Date 1476791809 -7200
# Node ID 4f11063c6e555492ba9f440f31915b1c51143d19
# Parent  0f000101652a98f39c02b1bbc2da700a5b8d71e6
clarified properties;

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