I wonder why your team decided to develop and use PyTorchBot to manage GitHub pull requests?
Are there any advantages to using this bot? Rather than just use GitHub built-in features?
Consider that some people might be confused about the bot’s action, like:
Thanks for the prompt response, but then why is the PR status ‘closed’ and not ‘merged’?
Which built-in features are you referring to?
The bot allows you to easily rebase, merge when all tests pass, force a merge and explain why a failing test can be ignored, revert PRs etc. with minimal effort.
One of the main reasons was that Github didn’t support a merge queue until recently
GitHub merge queue is generally available - The GitHub Blog and with the volume of PRs that get merged to Github it would be impossible to merge anything without it
Other nice features rebases and reverts which the team uses quite a bit and of course ignoring tests which you typically can’t do unless you’re an admin