more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
1.1 --- a/src/Pure/System/isabelle_system.scala Sun Nov 24 18:06:09 2013 +0100
1.2 +++ b/src/Pure/System/isabelle_system.scala Mon Nov 25 18:03:38 2013 +0100
1.3 @@ -302,11 +302,14 @@
1.4
1.5 private val pid = stdout.readLine
1.6
1.7 + private def kill_cmd(signal: String): Int =
1.8 + execute(true, "/bin/bash", "-c", "kill -" + signal + " -" + pid).waitFor
1.9 +
1.10 private def kill(signal: String): Boolean =
1.11 {
1.12 try {
1.13 - execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
1.14 - execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
1.15 + kill_cmd(signal)
1.16 + kill_cmd("0") == 0
1.17 }
1.18 catch { case _: InterruptedException => true }
1.19 }