From 2510f4363b88f095a8ad57eb9c4e64352ba83a75 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 8 Mar 2025 02:20:57 +0100 Subject: [PATCH] feat: export RpcSessionAtPos --- vscode-lean4/src/infoview.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index b6a5a6b97..b29b447d4 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -60,7 +60,7 @@ async function rpcConnect(client: LeanClient, uri: ls.DocumentUri): Promise