equal
deleted
inserted
replaced
181 } |
181 } |
182 |
182 |
183 |
183 |
184 // join |
184 // join |
185 |
185 |
186 def join: Int = |
186 def join(): Int = |
187 { |
187 { |
188 val rc = proc.waitFor |
188 val rc = proc.waitFor() |
189 do_cleanup() |
189 do_cleanup() |
190 rc |
190 rc |
191 } |
191 } |
192 |
192 |
193 |
193 |
216 } |
216 } |
217 } |
217 } |
218 } |
218 } |
219 |
219 |
220 val rc = |
220 val rc = |
221 try { join } |
221 try { join() } |
222 catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc } |
222 catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc } |
223 |
223 |
224 watchdog_thread.foreach(_.cancel()) |
224 watchdog_thread.foreach(_.cancel()) |
225 |
225 |
226 if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt() |
226 if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt() |