author | wenzelm |
Sat, 31 Dec 2016 15:18:04 +0100 | |
changeset 64724 | 44dbf8cc2d7f |
parent 64723 | 65bcb1fbaa73 |
child 64725 | 38305f56c769 |
--- a/src/Tools/VSCode/src/server.scala Sat Dec 31 14:35:37 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Dec 31 15:18:04 2016 +0100 @@ -306,7 +306,6 @@ update_document(uri, text) case Protocol.DidCloseTextDocument(uri) => close_document(uri) - case Protocol.DidSaveTextDocument(uri) => log("SAVE " + uri) case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case _ => log("### IGNORED")