src/Pure/ML-Systems/smlnj-0.93.ML
changeset 7855 092a6435afad
parent 7149 d0c2168f7704
child 12108 b6f10dcde803
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Oct 13 19:42:46 1999 +0200
@@ -90,7 +90,7 @@
 
 (* ML command execution *)
 
-fun use_text _ = System.Compile.use_stream o open_string;
+fun use_text _ _ = System.Compile.use_stream o open_string;
 
 
 
@@ -180,6 +180,9 @@
     result
   end;
 
+(*plain version; with return code*)
+fun system cmd = System.system cmd div 256;
+
 
 (* file handling *)