Zulip Chat Archive
Stream: mathlib4
Topic: !4#3039 or backport first?
Jeremy Tan (Mar 27 2023 at 13:53):
Which should be merged first, !4#3039 or the backport mathlib#18670?
Last updated: Dec 20 2023 at 11:08 UTC
Which should be merged first, !4#3039 or the backport mathlib#18670?
Last updated: Dec 20 2023 at 11:08 UTC