src/Pure/Tools/build_cluster.scala
changeset 78582 63f06b935a1f
parent 78581 1384593459b4
child 78584 92ef737f412c
equal deleted inserted replaced
78581:1384593459b4 78582:63f06b935a1f
   300     init()
   300     init()
   301     _init.foreach(_.join)
   301     _init.foreach(_.join)
   302 
   302 
   303     _workers =
   303     _workers =
   304       for (session <- _sessions) yield {
   304       for (session <- _sessions) yield {
   305         Future.thread(session.host.message("run")) {
   305         Future.thread(session.host.message("work")) {
   306           Exn.release(capture(session.host, "run") { session.start() })
   306           Exn.release(capture(session.host, "work") { session.start() })
   307         }
   307         }
   308       }
   308       }
   309   }
   309   }
   310 
   310 
   311   override def join: List[Build_Cluster.Result] = synchronized {
   311   override def join: List[Build_Cluster.Result] = synchronized {