strict EXEC_PROCESS: component can be expected to be present;
authorwenzelm
Thu, 05 Dec 2013 20:06:28 +0100
changeset 54677 ae5426994961
parent 54676 6b2ca4850b71
child 54678 87910da843d5
strict EXEC_PROCESS: component can be expected to be present;
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