Unable to pull from remote repository due to conflicting tag

Stream: mathlib4

[Kevin Buzzard]

Twice today I've tried to push some commits to a PR using VS Code and got the error

Unable to pull from remote repository due to conflicting tag(s): v4.9.0. Would you like to resolve the conflict by replacing the local tag(s)?

Seems to work fine from command line. What have I done wrong?

[Damiano Testa]

I've seen this too.

[Kim Morrison]

It seems the v4.9.0 tag was pushed when it should have been v4.9.0-rc1. Presumably this was my fault (although, worryingly, possibly not!). I overwrote it a few days ago when Mathlib actually moved to v4.9.0.

[Kim Morrison]

I've added tag protection rules, so if this happens again we can at least be certain that it was my (rather, some maintainer's) fault.