equal
deleted
inserted
replaced
22 |
22 |
23 /* properties */ |
23 /* properties */ |
24 |
24 |
25 object Prop |
25 object Prop |
26 { |
26 { |
|
27 val separator = '\u000b' |
|
28 |
27 def multiple(name: String, args: List[String]): Properties.T = |
29 def multiple(name: String, args: List[String]): Properties.T = |
28 if (args.isEmpty) Nil |
30 if (args.isEmpty) Nil |
29 else List(name -> YXML.string_of_body(XML.Encode.list(XML.Encode.string)(args))) |
31 else List(name -> args.mkString(separator.toString)) |
30 |
32 |
31 val build_tags = "build_tags" // multiple |
33 val build_tags = "build_tags" // multiple |
32 val build_args = "build_args" // multiple |
34 val build_args = "build_args" // multiple |
33 val build_group_id = "build_group_id" |
35 val build_group_id = "build_group_id" |
34 val build_id = "build_id" |
36 val build_id = "build_id" |