feat: address review #2638
Annotations
2 errors and 1 warning
|
Run tests
Type '{ InteractiveMessageData: (__0: { msg: { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; EditorContext: { Provider: (props: { value: { readonly api: { sendClientRequest: (uri: string, method: string, params: any) => Promise<...>; ... 11 more ...; closeRpcSessio...' does not satisfy the constraint '{ InteractiveMessageData: (__0: { msg: { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; EditorContext: { Provider: (props: { value: { readonly api: { ...; }; ... 5 more ...; requestPlainTermGoal: (pos: { ...; }) => Promise<...>; }; children?: string | ... 6 mo...'.
|
|
Run tests
The process 'C:\hostedtoolcache\windows\node\20.18.1\x64\npm.cmd' failed with exit code 1
|
|
Package
This extension consists of 1512 files, out of which 361 are JavaScript files. For performance reasons, you should bundle your extension: https://aka.ms/vscode-bundle-extension. You should also exclude unnecessary files by adding them to your .vscodeignore: https://aka.ms/vscode-vscodeignore.
|
Loading