# HG changeset patch
# User wenzelm
# Date 1399054075 -7200
# Node ID 93f05fa757dd6d880b547de7603bea6a4d138c7f
# Parent  e3ccf0809d513641cf0c6ce0f51718be9490b361
more redirection;

diff -r e3ccf0809d51 -r 93f05fa757dd src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:01:45 2014 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:07:55 2014 +0200
@@ -101,7 +101,11 @@
     global_console = console
     global_out = out
     global_err = if (err == null) out else err
-    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
+    val res = Exn.capture {
+      scala.Console.withErr(console_stream) {
+        scala.Console.withOut(console_stream) { e }
+      }
+    }
     console_stream.flush
     global_console = null
     global_out = null