diff options
| author | Eli Hughes <[email protected]> | 2025-04-26 13:04:39 -0400 |
|---|---|---|
| committer | Eli Hughes <[email protected]> | 2025-04-27 09:38:18 -0400 |
| commit | 0937a2b2d3dbc0b5595c6ea3a6acc8a691f73941 (patch) | |
| tree | a49cd33f586eedcd6d10c4c0a8121e22cb9ee8f6 | |
| parent | b5d4d0f6237ecaf78b2548e5c4a08810e0957066 (diff) | |
using get-deps from tinyuf2
| -rwxr-xr-x | tools/get_deps.py | 10 |
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") |
