From 09aa7c819ac4128619ace3c9142e751c3c5fac98 Mon Sep 17 00:00:00 2001
From: Will Thompson <wjt@endlessm.com>
Date: Mon, 24 Jun 2019 21:48:43 +0100
Subject: [PATCH] Prune tags as well

If we delete a tag, we probably have a good reason.
---
 update_repos | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/update_repos b/update_repos
index 9234593..962c85c 100755
--- a/update_repos
+++ b/update_repos
@@ -22,7 +22,7 @@ GITHUB_API_HOST = 'https://api.github.com'
 GIT_CLONE_CMD = 'git clone %s %s %s'
 GIT_CLONE_API_URL = 'https://%s@github.com/%s'
 GIT_SHA_CMD = 'git rev-parse --short %s'
-GIT_FETCH_CMD = 'git fetch --prune --tags'
+GIT_FETCH_CMD = 'git fetch --prune --tags --prune-tags'
 GIT_CHECK_REMOTE_CMD = 'git ls-remote'
 
 USER_DETAILS_PATH = '/users/%s'
-- 
GitLab