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 <doug@doughellmann.com>
This commit is contained in:
Doug Hellmann 2018-08-17 10:44:59 -04:00
parent 9a66c18e4e
commit 6263953264

View File

@ -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