more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
authorwenzelm
Wed May 22 16:01:08 2013 +0200 (2013-05-22 ago)
changeset 521123610ae73cfdb
parent 52111 1fd184eaa310
child 52113 2d2b049429f3
more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):
src/Pure/System/isabelle_system.scala
     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      }