diff --git a/tools/ci_fetch_deps.py b/tools/ci_fetch_deps.py index 491d8da0e5..55985ffe15 100644 --- a/tools/ci_fetch_deps.py +++ b/tools/ci_fetch_deps.py @@ -43,13 +43,15 @@ port_deps = { } -def run(title, command): +def run(title, command, check=True): print("::group::" + title, flush=True) print(command, flush=True) start = time.monotonic() - subprocess.run(shlex.split(command), stderr=subprocess.STDOUT) - print("Duration:", time.monotonic() - start, flush=True) - print("::endgroup::", flush=True) + try: + subprocess.run(shlex.split(command), stderr=subprocess.STDOUT, check=check) + finally: + print("Duration:", time.monotonic() - start, flush=True) + print("::endgroup::", flush=True) run( @@ -106,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",