[html] use NodeJS.Timer

This commit is contained in:
Martin Aeschlimann 2016-09-08 19:03:31 +02:00
parent d7bc41b908
commit 9717f397f5

View file

@ -80,7 +80,7 @@ documents.onDidClose(event => {
connection.sendDiagnostics({ uri: event.document.uri, diagnostics: [] });
});
let pendingValidationRequests : {[uri:string]:number} = {};
let pendingValidationRequests : {[uri:string]:NodeJS.Timer} = {};
const validationDelayMs = 200;
function cleanPendingValidation(textDocument: TextDocument): void {