Zulip Chat Archive
Stream: general
Topic: PR 16000
Yaël Dillies (Aug 10 2022 at 14:23):
Who wants to claim #16000?
Mauricio Collares (Aug 10 2022 at 14:32):
#16384 is another big one :)
Damiano Testa (Aug 10 2022 at 14:48):
Do you mean that anyone except whoever claims it should wait to make a new PR? I have never looked at the number and may have stepped unintentionally on someone toes... (not now, but possibly in the past, especially with the ubiquity of non-non-interesting numbers).
Yaël Dillies (Aug 10 2022 at 20:50):
It's rather whoever wants it who should monitor new PRs.
Violeta Hernández (Aug 11 2022 at 04:39):
Violeta Hernández (Aug 11 2022 at 04:39):
Funny how I missed #15000 and #16000 by only a few minutes each :stuck_out_tongue:
Mauricio Collares (Sep 03 2022 at 15:18):
Mauricio Collares said:
#16384 is another big one :)
20 PRs/issues away!
Junyan Xu (Oct 14 2022 at 22:57):
#17000 has landed :tada:
Yaël Dillies (Oct 14 2022 at 23:28):
What a big theorem!
Jireh Loreaux (Oct 15 2022 at 00:08):
Ha! Yeah, sorry about that. I wasn't even checking PR numbers.
Last updated: Dec 20 2023 at 11:08 UTC