# HG changeset patch
# User wenzelm
# Date 1489341002 -3600
# Node ID 187277b77d5080095a61768b37d10d155b97c6e7
# Parent  2d01b30e6ac69e242c3213d05b3aaf4c199da227
suppress vacuous messages;

diff -r 2d01b30e6ac6 -r 187277b77d50 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
       }
     }