max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix hasModule error message at parseTargetBaseSpec

Browse source
This commit is contained in:
tydeu 2021-10-10 12:52:49 -04:00
parent b8b3f01c96
commit 1074aaa5fa
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Cli.lean
View file

@ -286,7 +286,7 @@ def parseTargetBaseSpec (rootPkg : Package) (spec : String) : CliM (Package × O
if pkg.hasModule mod then
return (pkg, mod)
else
error s!"'{modStr}' is not a local module of package '{pkgStr}'"
error s!"package '{pkgStr}' has no module '{modStr}'"
| _ =>
error s!"invalid target spec '{spec}' (too many '/')"