src/Tools/VSCode/extension/src/extension.ts
changeset 65972 9f6a154c6ca0
parent 65970 05e317e291a8
child 65974 fd5f80ee2de0
--- a/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 14:43:42 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue May 30 15:29:42 2017 +0200
@@ -69,7 +69,7 @@
       if (editor) {
         const uri = editor.document.uri
         const cursor = editor.selection.active
-        if (uri.scheme === "file" && cursor)
+        if (library.is_file(uri) && cursor)
           caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
       }
       if (last_caret_update !== caret_update) {