# HG changeset patch
# User wenzelm
# Date 1482401338 -3600
# Node ID ea34f36ff6a5af9190bd3bd37677de9afbd9b520
# Parent  31b681e38c703ef722024a39d938edcc47bc8cb7
clarified message;

diff -r 31b681e38c70 -r ea34f36ff6a5 src/Tools/VSCode/src/server.scala
--- 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()