ignore message;
authorwenzelm
Sat Dec 31 15:18:04 2016 +0100 (2016-12-31)
changeset 6472444dbf8cc2d7f
parent 64723 65bcb1fbaa73
child 64725 38305f56c769
ignore message;
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/server.scala	Sat Dec 31 14:35:37 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:18:04 2016 +0100
     1.3 @@ -306,7 +306,6 @@
     1.4              update_document(uri, text)
     1.5            case Protocol.DidCloseTextDocument(uri) =>
     1.6              close_document(uri)
     1.7 -          case Protocol.DidSaveTextDocument(uri) => log("SAVE " + uri)
     1.8            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
     1.9            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    1.10            case _ => log("### IGNORED")