more redirection;
authorwenzelm
Fri May 02 20:07:55 2014 +0200 (2014-05-02)
changeset 5683293f05fa757dd
parent 56831 e3ccf0809d51
child 56833 d0a57abc71f8
more redirection;
src/Tools/jEdit/src/scala_console.scala
     1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:01:45 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 02 20:07:55 2014 +0200
     1.3 @@ -101,7 +101,11 @@
     1.4      global_console = console
     1.5      global_out = out
     1.6      global_err = if (err == null) out else err
     1.7 -    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
     1.8 +    val res = Exn.capture {
     1.9 +      scala.Console.withErr(console_stream) {
    1.10 +        scala.Console.withOut(console_stream) { e }
    1.11 +      }
    1.12 +    }
    1.13      console_stream.flush
    1.14      global_console = null
    1.15      global_out = null