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 *)