Here’s a quick git tip that I end up searching for it. There’s plenty of times we added git tags, pushed to remote, and realized that we named it wrong. Eg. v.0.1.0 instead of v0.1.0.
To change it back you would need to add a new tag and push it,
$> git tag new_tag old_tag (Eg. git tag v0.1.0 v.0.1.0)
$> git push --tags
Then delete the old tag from remote and local:
$> git push origin :refs/tags/old_tag
$> git tag -d old_tag
The colon in the push command removes the tag from the remote repository. If you do not do this, git will create the old tag on your machine when you pull.
Finally, make sure that the other users remove the deleted tag. Please tell them (co-workers) to run the following command:
$> git pull --prune --tags
Spread our Word!
