--- a/src/Tools/VSCode/extension/src/extension.ts Thu May 30 02:43:24 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Thu May 30 02:43:29 2024 +0200
@@ -198,8 +198,8 @@
language_client.onReady().then(() =>
{
context.subscriptions.push(
- window.onDidChangeActiveTextEditor(_ => update_caret()),
- window.onDidChangeTextEditorSelection(_ => update_caret()))
+ window.onDidChangeActiveTextEditor(update_caret),
+ window.onDidChangeTextEditorSelection(update_caret))
update_caret()
language_client.onNotification(lsp.caret_update_type, goto_file)