RELEASING.md: Add not on how to remove an incorrect tag #4114
Conversation
Signed-off-by: Stewart X Addison <[email protected]>
github-actions
bot
added
the
documentation
| Note: If you make a mistake with a tag you have already pushed you can undo it with: | ||
| ```bash | ||
| git tag --delete jdk-1.2.3-wrongname | ||
| git git push origin :jdk-1.2.3-wrongname |
There was a problem hiding this comment.
Should this say
git push origin jdk-1.2.3-rightname?
There was a problem hiding this comment.
No - the : specifically means "delete in the origin repository on github whereas the first command just deletes it on your local file system. Both are needed, and it doesn't replace the need to run the original commands to recreate and push the correct tag.
You can also use
git push --delete origin jdk-1.2.3-wrongname
instead of the : version - I could change it to that on the basis that it's probably clearer if you think that would be better (I just personally use : because it's shorter!)
There was a problem hiding this comment.
(Noting that you can also use -d as a shortened version of --delete but my gut feel is that in this document the longer one is clearer)
There was a problem hiding this comment.
I don't think you meant to repeat git in git git push ....
Also this adds a "note", not a "not.
There was a problem hiding this comment.
I see this has already been merged but I'll get a follow on to remove the duplicate git. Thanks.
Signed-off-by: Stewart X Addison <[email protected]>
|
Committers should also be able to delete tags from a browser view |
Hopefully self-explanatory. I had to do this during the January 2024 release so figured it's be useful to others to have this in the guide ;-)