# HG changeset patch # User wenzelm # Date 1543358497 -3600 # Node ID f557375f6e1718377f0adc6c325338f743fc5dc2 # Parent bff3eb77b0d1e5cf723da613290cff92e9fd2bc1 obsolete (see fc221fa79741); diff -r bff3eb77b0d1 -r f557375f6e17 src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Tue Nov 27 23:30:18 2018 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Tue Nov 27 23:41:37 2018 +0100 @@ -52,7 +52,6 @@ "inner_numeral", "inner_quoted", "inner_cartouche", - "inner_comment", "comment1", "comment2", "comment3",