fix: lengthen RPC reference field name #3031
Annotations
4 errors and 2 warnings
|
Linux
The process '/usr/bin/xvfb-run' failed with exit code 1
|
|
Linux
Type '{ InteractiveMessageData: (__0: { msg: { __rpcref: string; readonly [tag]: "Lean.MessageData"; } | { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; ... 44 more ...; InteractiveHypothesisBundle_nonAnonymousNames: (ih: { ...; }) => string[]; }' does not satisfy the constraint '{ InteractiveMessageData: (__0: { msg: { __rpcref: string; readonly [tag]: "Lean.MessageData"; } | { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; ... 44 more ...; InteractiveHypothesisBundle_nonAnonymousNames: (ih: { ...; }) => string[]; }'.
|
|
Windows
The process 'C:\hostedtoolcache\windows\node\24.14.0\x64\npm.cmd' failed with exit code 1
|
|
Windows
Type '{ InteractiveMessageData: (__0: { msg: { __rpcref: string; readonly [tag]: "Lean.MessageData"; } | { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; ... 44 more ...; InteractiveHypothesisBundle_nonAnonymousNames: (ih: { ...; }) => string[]; }' does not satisfy the constraint '{ InteractiveMessageData: (__0: { msg: { __rpcref: string; readonly [tag]: "Lean.MessageData"; } | { p: string; readonly [tag]: "Lean.MessageData"; }; }) => { type: any; props: any; key: string | null; }; ... 44 more ...; InteractiveHypothesisBundle_nonAnonymousNames: (ih: { ...; }) => string[]; }'.
|
|
Linux
This extension consists of 1097 files, out of which 243 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.
|
|
Windows
This extension consists of 1097 files, out of which 243 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.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
vscode-lean4
|
5.02 MB |
sha256:0f81b288eed5fefdbee6d0fc63b76575d37bfd41365f5f6b7a4a45446c0ba0b2
|
|