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

fix: make buildRec target wait for deps

Browse source
This commit is contained in:
tydeu 2021-11-05 14:12:58 -04:00
parent ffcf715f30
commit 57c7e42752
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Lake/BuildPackage.lean
View file

@ -87,7 +87,8 @@ def Package.buildRec (self : Package) [Inhabited i]
let recBuild := recBuildPackageWithDeps build
let targets ← failOnBuildCycle <| ← RBTopT.run' <|
buildRBTop (cmp := Name.quickCmp) recBuild Package.name self
targets.back
let target ← ActiveTarget.collectOpaqueArray targets
target.withInfo targets.back.info
/--
Build an `Array` of `Package`s along with their dependencies