src/Pure/Tools/build.scala
changeset 65284 d189ff34b5b9
parent 65282 f4c5f10829a0
child 65289 86d93effc3df
     1.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 09:49:01 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 10:03:00 2017 +0100
     1.3 @@ -204,7 +204,7 @@
     1.4    /* sources and heaps */
     1.5  
     1.6    sealed case class Session_Info(
     1.7 -    sources: String, input_heaps: String, output_heap: String, return_code: Int)
     1.8 +    sources: List[String], input_heaps: List[String], output_heap: String, return_code: Int)
     1.9  
    1.10    private val SOURCES = "sources: "
    1.11    private val INPUT_HEAP = "input_heap: "