On Wed, Sep 13, 2017 at 02:30:46PM -0700, Greg Kroah-Hartman wrote: > > Yes. I don't recall if it is a direct --force or if you would have to > > remove the original tag first (with git push <repo> :refs/tags/<tag>). > > Ah, but then if someone had pulled the old tag, they would have to > delete it locally before they can pull in the new one. That's the main > reason I'll not do this... In fact not, the tags are automatically replaced upon pull. I've been using such a crappy workflow for some time in the past, sharing human errors with coworkers... Git is pretty tolerant to this. It's just that it's terribly confusing because you can then have two people with the same tag name pointing to different commit IDs, I really hate this, it only works when all users are in the same office and you shout "sorry I messed up, I'm pushing the tag again". > Again, use the make command that we have just for this reason... It also has the benefit of always reporting the same version for all users including those only downloading the -rc patch. Willy