suppress vacuous messages;
authorwenzelm
Sun, 12 Mar 2017 18:50:02 +0100
changeset 65202 187277b77d50
parent 65201 2d01b30e6ac6
child 65203 314246c6eeaa
suppress vacuous messages;
src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 18:45:53 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sun Mar 12 18:50:02 2017 +0100
@@ -89,7 +89,8 @@
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {
-        client.sendNotification(protocol.caret_update_type, caret_update)
+        if (caret_update.uri)
+          client.sendNotification(protocol.caret_update_type, caret_update)
         last_caret_update = caret_update
       }
     }