We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 249f247 commit 6696d58Copy full SHA for 6696d58
scripts/mk_all.lean
@@ -30,7 +30,7 @@ def getLeanLibs : IO (Array String) := do
30
| throw <| IO.userError "failed to load Lake workspace"
31
let package := ws.root
32
let libs := (package.leanLibs.map (·.name)).map (·.toString)
33
- return if package.name == `mathlib then
+ return if package.baseName == `mathlib then
34
libs.erase "Cache" |>.erase "LongestPole" |>.erase "MathlibTest"
35
|>.push ("Mathlib".push pathSeparator ++ "Tactic")
36
else
0 commit comments