# HG changeset patch
# User wenzelm
# Date 1497294878 -7200
# Node ID 1700b74ebbb99365bf64e80d980d812039479a6c
# Parent  8bd8750a2f9b80b627eb05c6e2dfc9ba23c398bc
removed pointless entries: not part of api.LanguageEntry;

diff -r 8bd8750a2f9b -r 1700b74ebbb9 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 21:12:59 2017 +0200
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Jun 12 21:14:38 2017 +0200
@@ -103,8 +103,6 @@
 interface LanguageEntry
 {
   language: DocumentSelector
-  revealOn: string
-  adjustCursorMovement: boolean
   substitutions: Substitution[]
 }
 
@@ -138,8 +136,6 @@
           prettify_symbols_mode.exports.registerSubstitutions(
             {
               language: language,
-              revealOn: "none",
-              adjustCursorMovement: true,
               substitutions: substitutions
             }))
       }