Merge pull request #3100 from wavenumber-eng/get_deps_fix

Fixed broken deps on a fresh clone

1 files changed, 6 insertions, 4 deletions

diff --git a/tools/get_deps.py b/tools/get_deps.py
index ba9dc23ce..d89c1b2b1 100755
--- a/tools/get_deps.py
+++ b/tools/get_deps.py
@@ -243,11 +243,13 @@ def get_a_dep(d):
         p.mkdir(parents=True)
         run_cmd(f"{git_cmd} init")
         run_cmd(f"{git_cmd} remote add origin {url}")
+        head = None
+    else:
+        # Check if commit is already fetched
+        result = run_cmd(f"{git_cmd} rev-parse HEAD")
+        head = result.stdout.decode("utf-8").splitlines()[0]
+        run_cmd(f"{git_cmd} reset --hard")
 
-    # Check if commit is already fetched
-    result = run_cmd(f"{git_cmd} rev-parse HEAD")
-    head = result.stdout.decode("utf-8").splitlines()[0]
-    run_cmd(f"{git_cmd} reset --hard")
     if commit != head:
         run_cmd(f"{git_cmd} fetch --depth 1 origin {commit}")
         run_cmd(f"{git_cmd} checkout FETCH_HEAD")