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;

--- a/src/Pure/System/isabelle_system.scala	Sun Nov 24 18:06:09 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Nov 25 18:03:38 2013 +0100
@@ -302,11 +302,14 @@
 
     private val pid = stdout.readLine
 
+    private def kill_cmd(signal: String): Int =
+      execute(true, "/bin/bash", "-c", "kill -" + signal + " -" + pid).waitFor
+
     private def kill(signal: String): Boolean =
     {
       try {
-        execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
-        execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
+        kill_cmd(signal)
+        kill_cmd("0") == 0
       }
       catch { case _: InterruptedException => true }
     }