# HG changeset patch
# User wenzelm
# Date 1482944095 -3600
# Node ID 04806ad1e43a767644ebdcccb0f1fd1b8c2815dc
# Parent  7888be4fa4962edb844cf436f1a4bf2f69aa86c2
clarified protocol errors;

diff -r 7888be4fa496 -r 04806ad1e43a src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:49:47 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:54:55 2016 +0100
@@ -308,7 +308,7 @@
           case _ => channel.log("### IGNORED")
         }
       }
-      catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
+      catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     }
 
     @tailrec def loop()