PR #queue

Stream: general

[Yaël Dillies]

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

[Anne Baanen]

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

[Yaël Dillies]

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

[Scott Morrison]

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]

Yaël Dillies said:

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

241 :smiling_devil:

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

Down to 43

[Scott Morrison]

Down to 18!

[Scott Morrison]

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

[Scott Morrison]

11

[Scott Morrison]

11

[Eric Wieser]

Back up to 53 on the #queue!