diff options
Diffstat (limited to 'tools')
| -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") |