src/Pure/ML-Systems/multithreading_polyml.ML

 
     (*system thread*)
     val system_thread = Thread.fork (fn () =>
       let
         val status =
-          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
-            script_name ^ " " ^ pid_name ^ " " ^ output_name);
+          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
+            " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
         val res =
           (case Posix.Process.fromStatus status of
             Posix.Process.W_EXITED => Result 0
           | Posix.Process.W_EXITSTATUS 0wx82 => Signal
           | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)