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;
authorwenzelm
Mon, 25 Nov 2013 18:03:38 +0100
changeset 55294c19c83f49fa5
parent 55293 83cb91acebcc
child 55295 2b38549374ba
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;
src/Pure/System/isabelle_system.scala
     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      }