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; +