diff -r e3fc50c7da13 -r 4b0daca2bf88 src/Pure/Concurrent/bash_sequential.ML
--- a/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 21:53:11 2012 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML	Mon Apr 16 23:07:40 2012 +0200
@@ -7,7 +7,7 @@
 
 signature BASH =
 sig
-  val process: string -> {output: string, rc: int, terminate: unit -> unit}
+  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
 end;
 
 structure Bash: BASH =
@@ -17,16 +17,18 @@
   let
     val id = serial_string ();
     val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
-    val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
-    fun cleanup () = (try File.rm script_path; try File.rm output_path);
+    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+    fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
   in
     let
       val _ = File.write script_path script;
       val status =
         OS.Process.system
           ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
-            " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
-            File.shell_path output_path ^ "\"");
+            " script \"exec bash " ^ File.shell_path script_path ^
+            " > " ^ File.shell_path out_path ^
+            " 2> " ^ File.shell_path err_path ^ "\"");
       val rc =
         (case Posix.Process.fromStatus status of
           Posix.Process.W_EXITED => 0
@@ -34,9 +36,10 @@
         | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
         | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
 
-      val output = the_default "" (try File.read output_path);
+      val out = the_default "" (try File.read out_path);
+      val err = the_default "" (try File.read err_path);
       val _ = cleanup ();
-    in {output = output, rc = rc, terminate = fn () => ()} end
+    in {out = out, err = err, rc = rc, terminate = fn () => ()} end
     handle exn => (cleanup (); reraise exn)
   end;