src/Pure/ML-Systems/bash.ML
changeset 35023 16f9877abf0b
parent 35010 d6e492cea6e4
child 39576 48baf61cb888
     1.1 --- a/src/Pure/ML-Systems/bash.ML	Sun Feb 07 19:54:12 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/bash.ML	Sun Feb 07 20:21:38 2010 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4      val output_name = OS.FileSys.tmpName ();
     1.5  
     1.6      val status =
     1.7 -      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
     1.8 +      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
     1.9          script_name ^ " /dev/null " ^ output_name);
    1.10      val rc =
    1.11        (case Posix.Process.fromStatus status of