src/Pure/Concurrent/bash_sequential.ML
changeset 43850 7f2cbc713344
parent 43847 529159f81d06
child 44054 da5fcc0f6c52
--- a/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:52:41 2011 +0200
@@ -5,7 +5,10 @@
 could work via the controlling tty).
 *)
 
-fun bash_process script =
+structure Bash =
+struct
+
+fun process script =
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -32,3 +35,5 @@
     handle exn => (cleanup (); reraise exn)
   end;
 
+end;
+