Zulip Chat Archive
Stream: PR reviews
Topic: !4#4746
Jeremy Tan (Jun 06 2023 at 17:22):
I had not included the hack for lean4#2220 when I started working on !4#4738, and by the time I was told this !4#4738 had been merged, so I re-ported the file properly at !4#4746. I'd like it merged as soon as possible
Last updated: Dec 20 2023 at 11:08 UTC