Zulip Chat Archive
Stream: general
Topic: branch master'
Yury G. Kudryashov (Feb 25 2023 at 04:12):
Is it intentional that we have branch#master'?
Johan Commelin (Feb 25 2023 at 06:31):
It's the derivative of master, so it's a bit less smooth...
Yury G. Kudryashov (Feb 25 2023 at 19:50):
It is master from Jul 9, 2022
Yury G. Kudryashov (Feb 25 2023 at 19:50):
Should we delete it?
Yaël Dillies (Feb 25 2023 at 19:55):
Probably just an accident
Kevin Buzzard (Feb 25 2023 at 19:58):
More generally we should probably delete a gazillion branches
Yury G. Kudryashov (Feb 25 2023 at 20:50):
Deleted
Kevin Buzzard (Feb 25 2023 at 20:51):
(deleted)
Yury G. Kudryashov (Feb 25 2023 at 21:09):
OMG, we have 2117 branches.
Yury G. Kudryashov (Feb 25 2023 at 21:09):
In mathlib 3 repo
Yury G. Kudryashov (Feb 25 2023 at 21:10):
I'll cleanup some of my branches next week.
Thomas Browning (Feb 25 2023 at 22:11):
This came up previously: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/branches.20cleanup
Yaël Dillies (Feb 25 2023 at 22:13):
I regularly clean up branches but they keep getting more
Yaël Dillies (Feb 27 2023 at 08:28):
Yury G. Kudryashov said:
OMG, we have 2117 branches.
1934 now :downwards_trend:
Reid Barton (Feb 27 2023 at 08:31):
At this rate we will be all out of branches by next week!
Reid Barton (Feb 27 2023 at 08:33):
oh wait Feb 25 is not yesterday, please adjust estimate accordingly
Last updated: Dec 20 2023 at 11:08 UTC