# HG changeset patch
# User wenzelm
# Date 1369231268 -7200
# Node ID 3610ae73cfdbd1fa31431a3876cb35de7979f663
# Parent  1fd184eaa3107593ad44009ae7461327b4a9a825
more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):

diff -r 1fd184eaa310 -r 3610ae73cfdb src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed May 22 14:10:45 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed May 22 16:01:08 2013 +0200
@@ -305,8 +305,8 @@
     private def kill(signal: String): Boolean =
     {
       try {
-        execute(true, "kill", "-" + signal, "-" + pid).waitFor
-        execute(true, "kill", "-0", "-" + pid).waitFor == 0
+        execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
+        execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
       }
       catch { case _: InterruptedException => true }
     }