# HG changeset patch
# User wenzelm
# Date 1617827563 -7200
# Node ID 79761915770c94b4c0fcd36c686e9c505d347ca0
# Parent  f8c6c45cb11271c23cbd1a5572d5ef58058e6461
some tinkering with npm versions;

diff -r f8c6c45cb112 -r 79761915770c src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Wed Apr 07 22:28:41 2021 +0200
+++ b/src/Tools/VSCode/extension/package.json	Wed Apr 07 22:32:43 2021 +0200
@@ -543,7 +543,7 @@
     },
     "devDependencies": {
         "@types/mocha": "^2.2.48",
-        "@types/node": "^7.10.14",
+        "@types/node": "^10.11.0",
         "mocha": "^3.5.3",
         "typescript": "^3.9.9",
         "vscode": "^1.1.36"