Skip to content

doc: link the PR queue in the contribution guide - #897

Open
grunweg wants to merge 1 commit into
lean4from
grunweg-patch-2
Open

doc: link the PR queue in the contribution guide#897
grunweg wants to merge 1 commit into
lean4from
grunweg-patch-2

Conversation

@grunweg

@grunweg grunweg commented Aug 16, 2026

Copy link
Copy Markdown
Contributor

In general, PRs on the queue are more valuable to review. Also, a new contributor may otherwise think the list of all PRs is meaningful here (which can be confusing or overwhelming). Inspired by recent Zulip discussion.

In general, PRs on the queue are more valuable to review.
Also, a new contributor may otherwise think the list of all PRs is meaningful here (which can be confusing or overwhelming). Inspired by recent Zulip discussion.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant