--- a/src/Pure/ML-Systems/mlworks.ML Wed Oct 13 19:42:12 1999 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML Wed Oct 13 19:42:46 1999 +0200
@@ -78,7 +78,7 @@
(* ML command execution *)
(*Can one redirect 'use' directly to an instream?*)
-fun use_text _ txt =
+fun use_text _ _ txt =
let
val tmp_name = OS.FileSys.tmpName ();
val tmp_file = TextIO.openOut tmp_name;
@@ -121,6 +121,10 @@
result
end;
+(*plain version; with return code*)
+fun system cmd =
+ if OS.Process.system cmd = OS.Process.success then 0 else 1;
+
(* file handling *)