--- a/src/Pure/Concurrent/bash.ML Mon Aug 08 13:39:51 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML Mon Aug 08 13:40:24 2011 +0200
@@ -4,7 +4,12 @@
GNU bash processes, with propagation of interrupts.
*)
-structure Bash =
+signature BASH =
+sig
+ val process: string -> {output: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
struct
val process = uninterruptible (fn restore_attributes => fn script =>
--- a/src/Pure/Concurrent/bash_sequential.ML Mon Aug 08 13:39:51 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML Mon Aug 08 13:40:24 2011 +0200
@@ -5,7 +5,12 @@
could work via the controlling tty).
*)
-structure Bash =
+signature BASH =
+sig
+ val process: string -> {output: string, rc: int, terminate: unit -> unit}
+end;
+
+structure Bash: BASH =
struct
fun process script =