clarified multiple props: result needs to fit on a single line within the log file;
authorwenzelm
Tue Oct 18 14:32:51 2016 +0200 (2016-10-18)
changeset 643003073688abbe9
parent 64299 4f11063c6e55
child 64301 8053c882839f
clarified multiple props: result needs to fit on a single line within the log file;
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Tue Oct 18 13:56:49 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 14:32:51 2016 +0200
     1.3 @@ -202,8 +202,8 @@
     1.4        /* output log */
     1.5  
     1.6        val meta_info =
     1.7 -        Build_Log.Prop.lines(Build_Log.Prop.build_tags, build_tags) :::
     1.8 -        Build_Log.Prop.lines(Build_Log.Prop.build_args, build_args) :::
     1.9 +        Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
    1.10 +        Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args) :::
    1.11          List(
    1.12            Build_Log.Prop.build_group_id -> build_group_id,
    1.13            Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
     2.1 --- a/src/Pure/Admin/build_log.scala	Tue Oct 18 13:56:49 2016 +0200
     2.2 +++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 14:32:51 2016 +0200
     2.3 @@ -24,11 +24,12 @@
     2.4  
     2.5    object Prop
     2.6    {
     2.7 -    def lines(name: String, lines: List[String]): Properties.T =
     2.8 -      if (lines.isEmpty) Nil else List(name -> cat_lines(lines))
     2.9 +    def multiple(name: String, args: List[String]): Properties.T =
    2.10 +      if (args.isEmpty) Nil
    2.11 +      else List(name -> YXML.string_of_body(XML.Encode.list(XML.Encode.string)(args)))
    2.12  
    2.13 -    val build_tags = "build_tags"  // lines
    2.14 -    val build_args = "build_args"  // lines
    2.15 +    val build_tags = "build_tags"  // multiple
    2.16 +    val build_args = "build_args"  // multiple
    2.17      val build_group_id = "build_group_id"
    2.18      val build_id = "build_id"
    2.19      val build_engine = "build_engine"