--- 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),
--- 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"