src/Pure/ML-Systems/bash.ML
changeset 39576 48baf61cb888
parent 35023 16f9877abf0b
child 39583 c1e9c6dfeff8
     1.1 --- a/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:28:35 2010 +0200
     1.2 +++ b/src/Pure/ML-Systems/bash.ML	Mon Sep 20 23:36:26 2010 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4      val output_name = OS.FileSys.tmpName ();
     1.5  
     1.6      val status =
     1.7 -      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
     1.8 -        script_name ^ " /dev/null " ^ output_name);
     1.9 +      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^
    1.10 +        " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
    1.11      val rc =
    1.12        (case Posix.Process.fromStatus status of
    1.13          Posix.Process.W_EXITED => 0