Zulip Chat Archive

Stream: general

Topic: PSA for mathlib contributors


Simon Hudon (Mar 14 2019 at 06:09):

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 (Mar 14 2019 at 07:33):

That is... please run

git tag -d lean-3.4.2

if you have push access to community mathlib.

Simon Hudon (Mar 14 2019 at 07:34):

Thanks for supplying the details!

Kevin Buzzard (Mar 14 2019 at 07:46):

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

Johan Commelin (Mar 14 2019 at 07:46):

Yes, you need to remove the tag


Last updated: Dec 20 2023 at 11:08 UTC