I have attributed a tag called origin/v0.4.9
for a specific commit on a GitHub Pull Request. I thought the PR was simple, stable, and "a certainty" to be merged really fast. I was wrong.
I ended up extending the Pull Request - so the tag was kind of "deprecated" and stuck in the past. To make things worse, the PR was merged to main
branch.
Now, I want to associate the same tag (which uses the project notation) to a different commit.
Locally, in Magit (via Emacs) I deleted it (ok), on GitHub I successfully deleted it, and I tried adding a tag with the same on another commit, the latest one. It worked out locally. But, I can't push the addition. The mini-buffer returns:
tag 'origin/v0.4.9' already exists
How do I fix this?