feat: improve error messages when deps that should be shipped by default are not present - #780

feat: improve error messages when deps that should be shipped by default are not present#780

mhuisi merged 1 commit into

leanprover:masterleanprover/vscode-lean4:masterfrom

mhuisi:push-lxqzwkqkmwmnmhuisi/vscode-lean4:push-lxqzwkqkmwmnCopy head branch name to clipboard