1.1 --- a/src/Pure/Concurrent/bash.ML	Mon Aug 08 13:39:51 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/bash.ML	Mon Aug 08 13:40:24 2011 +0200
     1.3 @@ -4,7 +4,12 @@
     1.4  GNU bash processes, with propagation of interrupts.
     1.5  *)
     1.6  
     1.7 -structure Bash =
     1.8 +signature BASH =
     1.9 +sig
    1.10 +  val process: string -> {output: string, rc: int, terminate: unit -> unit}
    1.11 +end;
    1.12 +
    1.13 +structure Bash: BASH =
    1.14  struct
    1.15  
    1.16  val process = uninterruptible (fn restore_attributes => fn script =>

     2.1 --- a/src/Pure/Concurrent/bash_sequential.ML	Mon Aug 08 13:39:51 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/bash_sequential.ML	Mon Aug 08 13:40:24 2011 +0200
     2.3 @@ -5,7 +5,12 @@
     2.4  could work via the controlling tty).
     2.5  *)
     2.6  
     2.7 -structure Bash =
     2.8 +signature BASH =
     2.9 +sig
    2.10 +  val process: string -> {output: string, rc: int, terminate: unit -> unit}
    2.11 +end;
    2.12 +
    2.13 +structure Bash: BASH =
    2.14  struct
    2.15  
    2.16  fun process script =