# HG changeset patch
# User wenzelm
# Date 1497257306 -7200
# Node ID 5a00cec6bc8271a87f2a7b296010e7ff65414a88
# Parent  a2e441805d6a1408d80ad8eb87acc4ac7e9c771a
tuned;

diff -r a2e441805d6a -r 5a00cec6bc82 src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Sat Jun 10 22:50:40 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts	Mon Jun 12 10:48:26 2017 +0200
@@ -130,7 +130,7 @@
   if (document_uri) {
     const editor =
       window.visibleTextEditors.find(editor =>
-        editor.document.uri.scheme === document_uri.scheme &&
+        library.is_file(editor.document.uri) &&
         editor.document.uri.fsPath === document_uri.fsPath)
     if (editor) window.showTextDocument(editor.document, editor.viewColumn)
     else workspace.openTextDocument(document_uri).then(window.showTextDocument)