From 57fea2d8e33a61721fcf44f5aadb72178dc346cd Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 11 Mar 2023 00:59:55 +0000 Subject: [PATCH] feat: accept empty git hash as version Fixes leanprover/lake#154 --- Lake/Build/Monad.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean index 62bed905ed..0898eb05e9 100644 --- a/Lake/Build/Monad.lean +++ b/Lake/Build/Monad.lean @@ -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 :=