src/Pure/Concurrent/bash.ML
changeset 43850 7f2cbc713344
parent 43847 529159f81d06
child 44054 da5fcc0f6c52
--- 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;
+