From 0937a2b2d3dbc0b5595c6ea3a6acc8a691f73941 Mon Sep 17 00:00:00 2001 From: Eli Hughes Date: Sat, 26 Apr 2025 13:04:39 -0400 Subject: [PATCH] using get-deps from tinyuf2 --- tools/get_deps.py | 10 ++++++---- 1 file 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")