Zulip Chat Archive

Stream: general

Topic: PR #queue


Yaël Dillies (Sep 06 2021 at 10:52):

We've reached 240 open PRs! Pretty sure that's unprecedented :octopus:

Anne Baanen (Sep 06 2021 at 10:53):

I (ab)used my powers to add a link to the #queue to the title. Saves a bit of clicking :)

Yaël Dillies (Sep 06 2021 at 10:54):

Ahah! Was wondering how wizardly my mistyping had to be to have done that.

Scott Morrison (Sep 06 2021 at 11:07):

Just noting, of course, that while only a few of us can actually hit merge on a PR, everyone can contribute reviews, and we would love more reviews!

(In particular, when mathlib maintainers see comments like: "Thanks for fixing this up, it looks good to me now." written by people who've contributed previously, we can often make pretty short work of typing bors merge!)

Alex J. Best (Sep 06 2021 at 11:10):

Yaël Dillies said:

We've reached 240 open PRs! Pretty sure that's unprecedented :octopus:

241 :smiling_devil:

Scott Morrison (Sep 06 2021 at 11:12):

I'm not sure the 241 number is really relevant. Instead you should follow #queue and see how many (64?) are listed there.

Scott Morrison (Sep 06 2021 at 11:13):

We tend not to close semi-abandoned PRs, so there's a lot of clutter. (That said, in preparation for flag day for the port to Lean4 it won't hurt if people want to close --- or necro --- old PRs.)

Yaël Dillies (Sep 06 2021 at 11:50):

Still, the number of PR grew by ~40-50 in the last few days alone.

Scott Morrison (Sep 06 2021 at 12:01):

Well, 53 PRs on the #queue now, and I'm off to bed. :-)

Johan Commelin (Sep 06 2021 at 13:00):

Down to 43

Scott Morrison (Sep 07 2021 at 06:07):

Down to 18!

Scott Morrison (Sep 07 2021 at 06:08):

#8869 is now the only PR last touched before yesterday.

Scott Morrison (Sep 07 2021 at 09:06):

11

Scott Morrison (Sep 07 2021 at 09:06):

11

Eric Wieser (Sep 20 2021 at 17:28):

Back up to 53 on the #queue!


Last updated: Dec 20 2023 at 11:08 UTC