# HG changeset patch
# User wenzelm
# Date 1482334082 -3600
# Node ID 0b513620d94916140d61b756523d5c076a6f08cd
# Parent  7dbc9485ed70a9ff323a9fe91e4f754615c42291
proper pattern match;

diff -r 7dbc9485ed70 -r 0b513620d949 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:22:23 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 16:28:02 2016 +0100
@@ -243,7 +243,7 @@
         json match {
           case Protocol.Initialize(id) => init(id)
           case Protocol.Shutdown(id) => shutdown(id)
-          case Protocol.Exit => exit()
+          case Protocol.Exit(()) => exit()
           case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
             update_document(uri, text)
           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>