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