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

feat: accept empty git hash as version

Browse source 
Fixes leanprover/lake#154
This commit is contained in:
Gabriel Ebner 2023-03-11 00:59:55 +00:00 • committed by Mac
parent 276bf837e2
commit 57fea2d8e3
1 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Lake/Build/Monad.lean
View file

@ -13,11 +13,7 @@ namespace Lake
def mkBuildContext (ws : Workspace) (oldMode : Bool) : IO BuildContext := do
let lean := ws.lakeEnv.lean
let leanTrace :=
if lean.githash.isEmpty then
mixTrace (← computeTrace lean.lean) (← computeTrace lean.sharedLib)
else
Hash.ofString lean.githash
let leanTrace := Hash.ofString lean.githash
return {opaqueWs := ws, leanTrace, oldMode}
@[inline] def getLeanTrace : BuildM BuildTrace :=