src/Pure/ML-Systems/mosml.ML
changeset 35010 d6e492cea6e4
parent 34145 3dcb46ae6185
     1.1 --- a/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:39:33 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sat Feb 06 14:50:55 2010 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun system_out script =
     1.8 +fun bash_output script =
     1.9    let
    1.10      val script_name = OS.FileSys.tmpName ();
    1.11      val _ = write_file script_name script;