On Thu, Sep 14, 2017 at 04:18:03AM +0200, Willy Tarreau wrote: > 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. > It reports the same version, but it is not necessarily the same code. There are cases where a rc is updated, but not the Makefile. That happens quite a lot, actually. This is similar to mainline, which currently claims to be v4.13.0 until -rc1, then it claims to be -rc1 until -rc2, and so on. Guenter