Zulip Chat Archive
Stream: PR reviews
Topic: !3#19008 – should be ready
Jeremy Tan (Jun 29 2023 at 04:50):
As the title says. The awaiting-author issue has been resolved
Jeremy Tan (Jun 29 2023 at 04:51):
The porting of the file to mathlib4 is blocked by it
Mauricio Collares (Jun 29 2023 at 11:50):
Turns out there's a single requested wait left now: !3#19156
Eric Rodriguez (Jun 29 2023 at 12:04):
@Eric Wieser is on holiday for a while, so unsure what should be done about this
Eric Wieser (Jun 29 2023 at 12:16):
I'm happy for someone else to finish it off
Eric Wieser (Jun 29 2023 at 12:16):
The conflicts and requests for doc comments should be easy
Jeremy Tan (Jul 01 2023 at 03:14):
!4#5607 is ready for review
Last updated: Dec 20 2023 at 11:08 UTC