Zulip Chat Archive
Stream: mathlib4
Topic: !4#2447 Sum.Associator
Adam Topaz (Feb 28 2023 at 17:52):
This had a merge conflict and never got merged. The conflicts should all be resolved now. I also feel strange about merging it as the author of the PR... can someone else kickbitbon the queue?
Johan Commelin (Feb 28 2023 at 18:04):
In such cases, I don't think you should feel bad to kick it yourself.
Last updated: May 02 2025 at 03:31 UTC