Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4#572
Moritz Doll (Nov 13 2022 at 23:50):
@Scott Morrison since you are on a merging spree, could you merge this, too? I was about to correct some of these things again..
Last updated: May 02 2025 at 03:31 UTC