feat: [lean4web] export RpcSessionAtPos#586

joneugster wants to merge 1 commit into

leanprover:masterleanprover/vscode-lean4:masterfrom

hhu-adam:eugster/export_RpcSessionAtPoshhu-adam/vscode-lean4:eugster/export_RpcSessionAtPosCopy head branch name to clipboard