--- a/src/Pure/ML-Systems/bash.ML Mon Sep 20 23:28:35 2010 +0200
+++ b/src/Pure/ML-Systems/bash.ML Mon Sep 20 23:36:26 2010 +0200
@@ -25,8 +25,8 @@
val output_name = OS.FileSys.tmpName ();
val status =
- OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
- script_name ^ " /dev/null " ^ output_name);
+ OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^
+ " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
val rc =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => 0