# HG changeset patch
# User wenzelm
# Date 1496927550 -7200
# Node ID 98aaeff47795bd7dfa70a718df7dac66fdb27ae1
# Parent  c49bd8bb4839df766fbc705c0790670598e27f2d
clarified menu;
avoid non-portable ALT-mouse combination;

diff -r c49bd8bb4839 -r 98aaeff47795 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Thu Jun 08 14:27:13 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json	Thu Jun 08 15:12:30 2017 +0200
@@ -67,8 +67,12 @@
             "editor/title": [
                 {
                     "when": "editorLangId == isabelle",
+                    "command": "isabelle.preview",
+                    "group": "navigation"
+                },
+                {
+                    "when": "editorLangId == isabelle",
                     "command": "isabelle.preview-split",
-                    "alt": "isabelle.preview",
                     "group": "navigation"
                 },
                 {