equal
deleted
inserted
replaced
330 { |
330 { |
331 try { |
331 try { |
332 kill_cmd(signal) |
332 kill_cmd(signal) |
333 kill_cmd("0") == 0 |
333 kill_cmd("0") == 0 |
334 } |
334 } |
335 catch { case _: InterruptedException => true } |
335 catch { case Exn.Interrupt() => true } |
336 } |
336 } |
337 |
337 |
338 private def multi_kill(signal: String): Boolean = |
338 private def multi_kill(signal: String): Boolean = |
339 { |
339 { |
340 var running = true |
340 var running = true |
341 var count = 10 |
341 var count = 10 |
342 while (running && count > 0) { |
342 while (running && count > 0) { |
343 if (kill(signal)) { |
343 if (kill(signal)) { |
344 try { Thread.sleep(100) } catch { case _: InterruptedException => } |
344 try { Thread.sleep(100) } catch { case Exn.Interrupt() => } |
345 count -= 1 |
345 count -= 1 |
346 } |
346 } |
347 else running = false |
347 else running = false |
348 } |
348 } |
349 running |
349 running |
479 File.read_lines(proc.stderr, limited(progress_stderr)) |
479 File.read_lines(proc.stderr, limited(progress_stderr)) |
480 } |
480 } |
481 |
481 |
482 val rc = |
482 val rc = |
483 try { proc.join } |
483 try { proc.join } |
484 catch { case e: InterruptedException => proc.terminate; 130 } |
484 catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code } |
485 Bash_Result(stdout.join, stderr.join, rc) |
485 Bash_Result(stdout.join, stderr.join, rc) |
486 } |
486 } |
487 } |
487 } |
488 |
488 |
489 def bash(script: String): Bash_Result = bash_env(null, null, script) |
489 def bash(script: String): Bash_Result = bash_env(null, null, script) |