Skip to content

[feat infrastructure] Added actions scripts to count no. of reviewers#1451

Closed
Alex-Zughaid wants to merge 1 commit into
leanprover-community:masterfrom
Alex-Zughaid:github-reviewer-bot
Closed

[feat infrastructure] Added actions scripts to count no. of reviewers#1451
Alex-Zughaid wants to merge 1 commit into
leanprover-community:masterfrom
Alex-Zughaid:github-reviewer-bot

Conversation

@Alex-Zughaid

Copy link
Copy Markdown

Script to check: how many open PRs are in need of a reviewer; how many PRs each reviewer is currently assigned to, and updates on any PRs that were merged in the previous day.

Then send a message to the Zulip thread.

Secrets have been added to the repo.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@Alex-Zughaid
Alex-Zughaid marked this pull request as draft July 20, 2026 16:06
@Alex-Zughaid Alex-Zughaid changed the title [feat infrastructure] Added actioons scripts to count no. of reviewers [feat infrastructure] Added actions scripts to count no. of reviewers Jul 20, 2026
@github-actions github-actions Bot added the CI label Jul 20, 2026
@Alex-Zughaid
Alex-Zughaid deleted the github-reviewer-bot branch July 20, 2026 16:10
@Alex-Zughaid
Alex-Zughaid restored the github-reviewer-bot branch July 20, 2026 16:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant