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