diff -r e6226e100ac5 -r 529159f81d06 src/Pure/Concurrent/bash_sequential.ML
--- 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;