Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Ignores commands in PR description #84

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in 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