Skip to content

Ignores commands in PR description #84

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom
Open
RalfJung opened this issue Feb 29, 2020 · 1 comment · May be fixed by #211
Open

Ignores commands in PR description #84

RalfJung opened this issue Feb 29, 2020 · 1 comment · May be fixed by #211

Comments

@RalfJung
Copy link
Member

In some cases, a PR goes through bors as a matter of process but doesn't actually need any review -- for example this miri PR. In that case it would be nice if we could just have a bors command in the PR description, instead of having to submit the PR and then add a comment with the comment.
@RalfJung
Copy link
Member Author

FWIW, leaving bors commands in the initial post works with bors-ng.

@clubby789 clubby789 linked a pull request Mar 3, 2024 that will close this issue
Open
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Parse commands in PR comments clubby789/homu
1 participant
@RalfJung