# HG changeset patch
# User wenzelm
# Date 1312803624 -7200
# Node ID da5fcc0f6c520c84f07fa32bb020305e32bcb511
# Parent  3cc902f81a26a4f4775500291afea1dbd881293e
proper signature;

diff -r 3cc902f81a26 -r da5fcc0f6c52 src/Pure/Concurrent/bash.ML
--- 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 =>
diff -r 3cc902f81a26 -r da5fcc0f6c52 src/Pure/Concurrent/bash_sequential.ML
--- 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 =