--- a/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 18:11:14 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 18:20:02 2011 +0200
@@ -5,7 +5,7 @@
could work via the controlling tty).
*)
-fun bash_output script =
+fun bash_process script =
let
val id = serial_string ();
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -28,7 +28,7 @@
val output = the_default "" (try File.read output_path);
val _ = cleanup ();
- in (output, rc) end
+ in {output = output, rc = rc, terminate = fn () => ()} end
handle exn => (cleanup (); reraise exn)
end;