--- a/src/Tools/VSCode/extension/src/decorations.ts Tue May 30 15:29:42 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue May 30 15:30:00 2017 +0200
@@ -1,6 +1,6 @@
'use strict';
-import * as timers from 'timers';
+import * as timers from 'timers'
import { window, OverviewRulerLane } from 'vscode'
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
@@ -200,7 +200,7 @@
}
-/* decorations vs. document changes */
+/* handle document changes */
const touched_documents = new Set<TextDocument>()