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
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: May 11 2021 at 00:31 UTC