# HG changeset patch # User Thomas Lindae # Date 1717029809 -7200 # Node ID fdc1281430ebef1580d6eb90ad1a12efbef40050 # Parent befb2b4bffb3ffd883f34afa6c8f486babc57d93 vscode: tuned; diff -r befb2b4bffb3 -r fdc1281430eb src/Tools/VSCode/extension/src/extension.ts --- 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)