src/Pure/Admin/build_log.scala
changeset 64299 4f11063c6e55
parent 64298 0f000101652a
child 64300 3073688abbe9
     1.1 --- a/src/Pure/Admin/build_log.scala	Tue Oct 18 13:44:54 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 13:56:49 2016 +0200
     1.3 @@ -24,7 +24,11 @@
     1.4  
     1.5    object Prop
     1.6    {
     1.7 -    val build_tags = "build_tags"
     1.8 +    def lines(name: String, lines: List[String]): Properties.T =
     1.9 +      if (lines.isEmpty) Nil else List(name -> cat_lines(lines))
    1.10 +
    1.11 +    val build_tags = "build_tags"  // lines
    1.12 +    val build_args = "build_args"  // lines
    1.13      val build_group_id = "build_group_id"
    1.14      val build_id = "build_id"
    1.15      val build_engine = "build_engine"