# HG changeset patch
# User wenzelm
# Date 1386270388 -3600
# Node ID ae5426994961e9060ec955cd83a383e48596cfeb
# Parent  6b2ca4850b71e68c807d4c393a24823f53373203
strict EXEC_PROCESS: component can be expected to be present;

diff -r 6b2ca4850b71 -r ae5426994961 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Thu Dec 05 19:59:43 2013 +0100
+++ b/src/Pure/Concurrent/bash.ML	Thu Dec 05 20:06:28 2013 +0100
@@ -40,14 +40,10 @@
                 File.shell_path script_path ^
                 " > " ^ File.shell_path out_path ^
                 " 2> " ^ File.shell_path err_path;
+            val _ = getenv_strict "EXEC_PROCESS";
             val status =
               OS.Process.system
-                (if getenv "EXEC_PROCESS" = "" then
-                  ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
-                    File.shell_path pid_path ^ " script " ^ quote bash_script)
-                 else
-                  ("exec \"$EXEC_PROCESS\" " ^
-                    File.shell_path pid_path ^ " " ^ quote bash_script));
+                ("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script);
             val res =
               (case Posix.Process.fromStatus status of
                 Posix.Process.W_EXITED => Result 0