src/Pure/Admin/build_log.scala
changeset 64303 605351c7ef97
parent 64300 3073688abbe9
child 64341 45b6faeee56d
     1.1 --- a/src/Pure/Admin/build_log.scala	Tue Oct 18 15:18:58 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 15:31:08 2016 +0200
     1.3 @@ -24,9 +24,11 @@
     1.4  
     1.5    object Prop
     1.6    {
     1.7 +    val separator = '\u000b'
     1.8 +
     1.9      def multiple(name: String, args: List[String]): Properties.T =
    1.10        if (args.isEmpty) Nil
    1.11 -      else List(name -> YXML.string_of_body(XML.Encode.list(XML.Encode.string)(args)))
    1.12 +      else List(name -> args.mkString(separator.toString))
    1.13  
    1.14      val build_tags = "build_tags"  // multiple
    1.15      val build_args = "build_args"  // multiple