From 42ea5f226ba7892949a437e641ed87fadd90df0e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sat, 14 May 2022 15:42:37 +0200
Subject: [PATCH] fix: do not call git checkout unless necessary

See #63.
---
 Lake/Config/Resolve.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean
index c3e12c2949bc0..4aac201363168 100644
--- 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