Script to delete bad tags from the repo (#347)

faucetsdn · Jun 2, 2022 · 149506f · 149506f
1 parent 7a9fa2b
commit 149506f
Showing 1 changed file with 18 additions and 0 deletions.
diff --git a/bin/clean_tags b/bin/clean_tags
@@ -0,0 +1,18 @@
+#!/bin/bash -e
+
+if [[ -n $1 ]]; then
+    repo=$1
+    shift
+    git fetch $repo --tags
+fi
+
+for tag in $(git tag); do
+    # A bad tag is one that does not have a common parent with master branch.
+    merge=$(git merge-base $tag master || true)
+    if [[ -z $merge ]]; then
+        git tag -d $tag
+        if [[ -n $repo ]]; then
+            git push $repo :$tag
+        fi
+    fi
+done