1.1 --- a/src/Pure/Concurrent/bash.ML	Thu Dec 05 19:59:43 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.ML	Thu Dec 05 20:06:28 2013 +0100
     1.3 @@ -40,14 +40,10 @@
     1.4                  File.shell_path script_path ^
     1.5                  " > " ^ File.shell_path out_path ^
     1.6                  " 2> " ^ File.shell_path err_path;
     1.7 +            val _ = getenv_strict "EXEC_PROCESS";
     1.8              val status =
     1.9                OS.Process.system
    1.10 -                (if getenv "EXEC_PROCESS" = "" then
    1.11 -                  ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
    1.12 -                    File.shell_path pid_path ^ " script " ^ quote bash_script)
    1.13 -                 else
    1.14 -                  ("exec \"$EXEC_PROCESS\" " ^
    1.15 -                    File.shell_path pid_path ^ " " ^ quote bash_script));
    1.16 +                ("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script);
    1.17              val res =
    1.18                (case Posix.Process.fromStatus status of
    1.19                  Posix.Process.W_EXITED => Result 0