fix: do not call git checkout unless necessary

See leanprover#63.
Kha · May 15, 2022 · 42ea5f2 · 42ea5f2
1 parent 85b1c0f
commit 42ea5f2
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean
@@ -21,8 +21,9 @@ cloning and/or updating it as necessary.
 def materializeGit
 (name : String) (dir : FilePath) (url rev : String) : (LogT IO) PUnit := do
   if ← dir.isDir then
-    logInfo s!"{name}: trying to update {dir} to revision {rev}"
     let hash ← parseOriginRevision rev dir
+    if (← headRevision dir) == hash then return
+    logInfo s!"{name}: trying to update {dir} to revision {rev}"
     unless ← revisionExists hash dir do fetch dir
     checkoutDetach hash dir
   else