equal
deleted
inserted
replaced
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 |