# HG changeset patch
# User wenzelm
# Date 1456838604 -3600
# Node ID 4759dbb35148d0fa0e608c9f668da5064587b4bf
# Parent  c13dac251a810fdf55cf08ea38595f176c46c39b
prefer bash_process;

diff -r c13dac251a81 -r 4759dbb35148 src/Pure/Concurrent/bash_windows.ML
--- a/src/Pure/Concurrent/bash_windows.ML	Tue Mar 01 12:59:46 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML	Tue Mar 01 14:23:24 2016 +0100
@@ -12,10 +12,6 @@
 structure Bash: BASH =
 struct
 
-fun cygwin_bash arg =
-  let val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"
-  in Windows.simpleExecute (cmd, quote cmd ^ " -c " ^ quote arg) end;
-
 val process = uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
@@ -39,12 +35,15 @@
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
+            val bash_script =
+              "bash " ^ File.shell_path script_path ^
+                " > " ^ File.shell_path out_path ^
+                " 2> " ^ File.shell_path err_path;
+            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
             val rc =
-              cygwin_bash
-                ("echo $$ > " ^ File.shell_path pid_path ^ "; exec bash " ^
-                  File.shell_path script_path ^
-                  " > " ^ File.shell_path out_path ^
-                  " 2> " ^ File.shell_path err_path)
+              Windows.simpleExecute ("",
+                quote (ML_System.platform_path bash_process) ^ " " ^
+                quote (File.platform_path pid_path) ^ " bash -c " ^ quote bash_script)
               |> Windows.fromStatus |> SysWord.toInt;
             val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
           in Synchronized.change result (K res) end
@@ -61,8 +60,14 @@
       | terminate (SOME pid) =
           let
             fun kill s =
-              OS.Process.isSuccess (cygwin_bash ("kill -" ^ s ^ " -" ^ string_of_int pid))
-                handle OS.SysErr _ => false;
+              let
+                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+              in
+                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+                  handle OS.SysErr _ => false
+              end;
+
             fun multi_kill count s =
               count = 0 orelse
                 (kill s; kill "0") andalso