src/Pure/ML-Systems/multithreading_polyml.ML
changeset 35010 d6e492cea6e4
parent 33219 a69147d95957
child 35023 16f9877abf0b
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:39:33 2010 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 06 14:50:55 2010 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    val interruptible: ('a -> 'b) -> 'a -> 'b
     1.6    val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
     1.7 -  val system_out: string -> string * int
     1.8 +  val bash_output: string -> string * int
     1.9    structure TimeLimit: TIME_LIMIT
    1.10  end;
    1.11  
    1.12 @@ -156,9 +156,9 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* system shell processes, with propagation of interrupts *)
    1.17 +(* GNU bash processes, with propagation of interrupts *)
    1.18  
    1.19 -fun system_out script = with_attributes no_interrupts (fn orig_atts =>
    1.20 +fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
    1.21    let
    1.22      val script_name = OS.FileSys.tmpName ();
    1.23      val _ = write_file script_name script;