src/Pure/Concurrent/bash_sequential.ML
changeset 44054 da5fcc0f6c52
parent 43850 7f2cbc713344
child 47499 4b0daca2bf88
--- 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 =