Skip to content

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

Merged
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-lxqzwkqkmwmn
May 29, 2026
Merged

feat: improve error messages when deps that should be shipped by default are not present#780
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-lxqzwkqkmwmn