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: May 02 2025 at 03:31 UTC
Which should be merged first, !4#3039 or the backport mathlib#18670?
Last updated: May 02 2025 at 03:31 UTC