From 332af4c26256071292288512bb1cb260e1bd3afe Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 22 Aug 2021 03:40:09 -0400 Subject: [PATCH] refactor: check hash after verifying module artifact exists --- Lake/BuildModule.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index 90ba69da24..5c378dc91e 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -76,9 +76,9 @@ def checkModuleTrace [GetMTime a] (artifact : a) let leanHash := Hash.compute contents let maxMTime := max leanMTime depTrace.mtime let fullHash := Hash.mix leanHash depTrace.hash - let sameHash ← checkIfSameHash fullHash hashFile try discard <| getMTime artifact -- ensure the artifact actually exists + let sameHash ← checkIfSameHash fullHash hashFile let mtime := ite sameHash 0 maxMTime (sameHash, ⟨fullHash, mtime⟩) catch _ =>