From 626395326484783215b2eabffb2e08f570630ac6 Mon Sep 17 00:00:00 2001 From: Doug Hellmann Date: Fri, 17 Aug 2018 10:44:59 -0400 Subject: [PATCH] prune dead branches on clone When we clone the repo, if we got a version from a local cache we may need to prune dead branches. Change-Id: I94e5856a3f21a4fe069b3450427514bc82d18614 Signed-off-by: Doug Hellmann --- tools/clone_repo.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/clone_repo.sh b/tools/clone_repo.sh index 1c878fe..7a795b0 100755 --- a/tools/clone_repo.sh +++ b/tools/clone_repo.sh @@ -172,7 +172,7 @@ fi # Make sure it is up to date compared to the upstream remote. (cd $local_dir && - git fetch origin --tags + git fetch origin --tags --prune ) if [ ! -z "$REF" ]; then