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

fix: only write manifest if a package was resolved

Browse source
This commit is contained in:
tydeu 2022-05-23 20:28:36 -04:00
parent e8d59a7a6e
commit c1b4074d54
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/CLI/Main.lean
View file

@ -114,7 +114,8 @@ def loadWorkspace (args : List String := []) (updateDeps := true) : CliStateM Wo
pure {}
let (packageMap, resolveMap) ←
resolveDeps ws pkg updateDeps |>.run manifest |>.run LogMethods.eio (m := IO)
IO.FS.writeFile ws.manifestFile <| Json.pretty <| toJson <| Manifest.fromMap resolveMap
unless resolveMap.isEmpty do
IO.FS.writeFile ws.manifestFile <| Json.pretty <| toJson <| Manifest.fromMap resolveMap
let packageMap := packageMap.insert pkg.name pkg
return {ws with packageMap}