--- a/src/Pure/Concurrent/bash.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML Sat Jul 16 20:52:41 2011 +0200
@@ -4,7 +4,10 @@
GNU bash processes, with propagation of interrupts.
*)
-val bash_process = uninterruptible (fn restore_attributes => fn script =>
+structure Bash =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
@@ -83,3 +86,5 @@
handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
end);
+end;
+