diff --git a/tools/ci_fetch_deps.py b/tools/ci_fetch_deps.py index 44295a06e9..55985ffe15 100644 --- a/tools/ci_fetch_deps.py +++ b/tools/ci_fetch_deps.py @@ -43,12 +43,12 @@ port_deps = { } -def run(title, command): +def run(title, command, check=True): print("::group::" + title, flush=True) print(command, flush=True) start = time.monotonic() try: - subprocess.run(shlex.split(command), stderr=subprocess.STDOUT, check=True) + subprocess.run(shlex.split(command), stderr=subprocess.STDOUT, check=check) finally: print("Duration:", time.monotonic() - start, flush=True) print("::endgroup::", flush=True) @@ -108,7 +108,11 @@ if submodules: submodules = " ".join(submodules) # This line will fail because the submodule's need different commits than the tip of the branch. We # fix it later. - run("Init the submodules we'll need", f"git submodule update --init -N --depth 1 {submodules}") + run( + "Init the submodules we'll need", + f"git submodule update --init -N --depth 1 {submodules}", + check=False, + ) run( "Fetch the submodule sha",