src/Pure/Tools/build.scala
changeset 59136 c2b23cb8a677
parent 59083 88b0b1f28adc
child 59319 677615cba30d
     1.1 --- a/src/Pure/Tools/build.scala	Thu Dec 11 15:24:28 2014 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Dec 11 23:31:30 2014 +0100
     1.3 @@ -345,9 +345,7 @@
     1.4        val graph = tree.graph
     1.5        val sessions = graph.keys
     1.6  
     1.7 -      val timings =
     1.8 -        sessions.par.map((name: String) =>
     1.9 -          Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
    1.10 +      val timings = Par_List.map((name: String) => (name, load_timings(name)), sessions)
    1.11        val command_timings =
    1.12          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    1.13        val session_timing =