changeset 64655 | ea34f36ff6a5 |
parent 64651 | ea5620f7b0d8 |
child 64667 | cdb0d559a24b |
--- a/src/Tools/VSCode/src/server.scala Wed Dec 21 23:54:21 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Thu Dec 22 11:08:58 2016 +0100 @@ -275,7 +275,7 @@ case _ => channel.log("### IGNORED") } } - catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) } + catch { case exn: Throwable => channel.error_message(Exn.message(exn)) } } @tailrec def loop()