# HG changeset patch
# User wenzelm
# Date 1456833586 -3600
# Node ID c13dac251a810fdf55cf08ea38595f176c46c39b
# Parent  f2e8984adef7a8ac9a0dfa96cfd6d828a6770b06
only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);

diff -r f2e8984adef7 -r c13dac251a81 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Tue Mar 01 10:32:55 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML	Tue Mar 01 12:59:46 2016 +0100
@@ -35,16 +35,13 @@
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
-            val bash_script =
-              "exec bash " ^
-                File.shell_path script_path ^
-                " > " ^ File.shell_path out_path ^
-                " 2> " ^ File.shell_path err_path;
             val _ = getenv_strict "ISABELLE_BASH_PROCESS";
             val status =
               OS.Process.system
                 ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.shell_path pid_path ^
-                  " bash -c " ^ quote bash_script);
+                  " bash " ^ File.shell_path script_path ^
+                  " > " ^ File.shell_path out_path ^
+                  " 2> " ^ File.shell_path err_path);
             val res =
               (case Posix.Process.fromStatus status of
                 Posix.Process.W_EXITED => Result 0