diff options
Diffstat (limited to 'editors/vscode/client/extension.js')
| -rw-r--r-- | editors/vscode/client/extension.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/editors/vscode/client/extension.js b/editors/vscode/client/extension.js index 3846eca..cd497d8 100644 --- a/editors/vscode/client/extension.js +++ b/editors/vscode/client/extension.js @@ -185,7 +185,7 @@ function shortKey(key) { function serverStampFor(bin) { if (bin) return fileStamp(bin); const dir = path.join(__dirname, '..', 'server'); - return sha256(['lsp.wasm', 'lsp.json', 'tinyvm.js'].map(f => fileStamp(path.join(dir, f))).join(',')); + return sha256(['lsp.wasm', 'lsp.json', 'lsp.bin', 'tinyvm.js'].map(f => fileStamp(path.join(dir, f))).join(',')); } // the key of a document as it is now, and what it reads (for checking it again when one of those changes) |