# HG changeset patch
# User wenzelm
# Date 1496151000 -7200
# Node ID 84ea75759b77d03f3159d3e04a7f08678f324027
# Parent  9f6a154c6ca02b2091e4519c49eb66920b73c1c2
tuned;

diff -r 9f6a154c6ca0 -r 84ea75759b77 src/Tools/VSCode/extension/src/decorations.ts
--- 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>()