more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
1.1 --- a/src/Pure/System/isabelle_system.scala Wed May 22 14:10:45 2013 +0200
1.2 +++ b/src/Pure/System/isabelle_system.scala Wed May 22 16:01:08 2013 +0200
1.3 @@ -305,8 +305,8 @@
1.4 private def kill(signal: String): Boolean =
1.5 {
1.6 try {
1.7 - execute(true, "kill", "-" + signal, "-" + pid).waitFor
1.8 - execute(true, "kill", "-0", "-" + pid).waitFor == 0
1.9 + execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
1.10 + execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
1.11 }
1.12 catch { case _: InterruptedException => true }
1.13 }