--- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Feb 06 14:39:33 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Feb 06 14:50:55 2010 +0100
@@ -8,7 +8,7 @@
sig
val interruptible: ('a -> 'b) -> 'a -> 'b
val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
- val system_out: string -> string * int
+ val bash_output: string -> string * int
structure TimeLimit: TIME_LIMIT
end;
@@ -156,9 +156,9 @@
end;
-(* system shell processes, with propagation of interrupts *)
+(* GNU bash processes, with propagation of interrupts *)
-fun system_out script = with_attributes no_interrupts (fn orig_atts =>
+fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
let
val script_name = OS.FileSys.tmpName ();
val _ = write_file script_name script;