Zulip Chat Archive

Stream: general

Topic: PSA for mathlib contributors


view this post on Zulip 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-

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Mar 14 2019 at 07:34):

Thanks for supplying the details!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Mar 14 2019 at 07:46):

Yes, you need to remove the tag


Last updated: May 11 2021 at 00:31 UTC