# HG changeset patch
# User wenzelm
# Date 1482334354 -3600
# Node ID 805c5e6fa430da59177a0c01dc0b1b303ec0d27e
# Parent  0b513620d94916140d61b756523d5c076a6f08cd
tuned messages;

diff -r 0b513620d949 -r 805c5e6fa430 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:28:02 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:32:34 2016 +0100
@@ -179,7 +179,10 @@
       })
   }
 
-  def exit() { sys.exit(if (state.value.session.isDefined) 1 else 0) }
+  def exit() {
+    channel.log("\n")
+    sys.exit(if (state.value.session.isDefined) 1 else 0)
+  }
 
 
   /* document management */
@@ -235,7 +238,7 @@
 
   def start()
   {
-    channel.log("\nServer started " + Date.now())
+    channel.log("Server started " + Date.now())
 
     def handle(json: JSON.T)
     {