Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Script to delete bad tags from the repo #347

Merged
merged 6 commits into from
Jun 2, 2022
Merged

Script to delete bad tags from the repo #347

Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cc42630
Slight shell tweaks to be more explicit about comparisons. Related to
johnrandolph Apr 19, 2022
a724f32
Adding clean tag script
grafnu Jun 1, 2022
ddf6bf3
UPdate script
grafnu Jun 1, 2022
85f64ad
Merge branch 'master' into tagdel
grafnu Jun 1, 2022
e3dc924
Fetch before clean
grafnu Jun 1, 2022
f62ca30
Comments
grafnu Jun 2, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 19 additions & 0 deletions bin/clean_tags
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
#!/bin/bash -e

repo=$1
shift || true
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's this for?


if [[ -n $repo ]]; then
git fetch $repo --tags
fi

for tag in `git tag`; do
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

New, better style is $() not `` (backtics)

# 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