# HG changeset patch
# User wenzelm
# Date 1440589404 -7200
# Node ID 636b578bfaddd9fd09c904b1c3d820cba1f4236d
# Parent  7b7f01afab71214633d5dcffa343fcf52d8da5a0
clarified kill on Windows: just one executable;

diff -r 7b7f01afab71 -r 636b578bfadd src/Pure/Concurrent/bash.scala
--- a/src/Pure/Concurrent/bash.scala	Tue Aug 25 16:49:14 2015 +0200
+++ b/src/Pure/Concurrent/bash.scala	Wed Aug 26 13:43:24 2015 +0200
@@ -60,12 +60,10 @@
 
     private val pid = stdout.readLine
 
-    private def kill_cmd(signal: String): Int =
-      Isabelle_System.execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid)
-        .waitFor
-
     private def kill(signal: String): Boolean =
-      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
+      Exn.Interrupt.postpone {
+        Isabelle_System.kill(signal, pid)
+        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
 
     private def multi_kill(signal: String): Boolean =
     {
diff -r 7b7f01afab71 -r 636b578bfadd src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Aug 25 16:49:14 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Aug 26 13:43:24 2015 +0200
@@ -290,6 +290,18 @@
   }
 
 
+  /* kill */
+
+  def kill(signal: String, group_pid: String): (String, Int) =
+  {
+    val bash =
+      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
+      else List("/usr/bin/env", "bash")
+    val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
+    process_output(raw_execute(null, null, true, cmdline: _*))
+  }
+
+
   /* bash */
 
   private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])