PSA for mathlib contributors

Stream: general

[Simon Hudon]

The nightly release system gets broken routinely because some people keep pushing the defunct lean-3.4.2 tag. Please check the tags in your local workspaces and delete the useless ones to avoid pushing them by accident. Due to early versions of the release system, you may have the lean-3.4.2 tag, or any tag beginning with bin-, nightly- or untagged-

[Johan Commelin]

That is... please run

git tag -d lean-3.4.2

if you have push access to community mathlib.

[Simon Hudon]

Thanks for supplying the details!

[Kevin Buzzard]

Oh, I did git branch -d lean-3.4.2. Do I need to do something else?

[Johan Commelin]

Yes, you need to remove the tag