--- 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)
{