src/Pure/Tools/build_cluster.scala
changeset 78506 14da1177d1c3
parent 78505 8cd399b25dac
child 78508 ab07d4cb7d1c
equal deleted inserted replaced
78505:8cd399b25dac 78506:14da1177d1c3
   224     _rc.synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
   224     _rc.synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
   225 
   225 
   226   def capture[A](host: Build_Cluster.Host, op: String)(
   226   def capture[A](host: Build_Cluster.Host, op: String)(
   227     e: => A,
   227     e: => A,
   228     msg: String = host.message(op + " ..."),
   228     msg: String = host.message(op + " ..."),
   229     err: Throwable => String = { exn => return_code(exn); host.message("failed to " + op) }
   229     err: Throwable => String = { exn =>
       
   230       return_code(exn)
       
   231       host.message("failed to " + op + "\n" + Exn.print(exn))
       
   232     }
   230   ): Exn.Result[A] = {
   233   ): Exn.Result[A] = {
   231     progress.capture(e, msg = msg, err = err)
   234     progress.capture(e, msg = msg, err = err)
   232   }
   235   }
   233 
   236 
   234 
   237