Skip to content

triagebot: tweak wording for miri changes message #159463

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

Merged
rust-bors merged 1 commit into from
Jul 18, 2026
Merged

triagebot: tweak wording for miri changes message #159463

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions triagebot.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1182,10 +1182,10 @@ new or modified directive in `src/doc/rustc-dev-guide/`.

[mentions."src/tools/miri"]
message = """
`miri` is developed in its own repository. If possible, consider \
making this change to \
[rust-lang/miri](https://github.com/rust-lang/miri) \
instead.
`miri` is developed in its own repository. If the Miri part of this change \
can be broken out, consider making this change to \
[rust-lang/miri](https://github.com/rust-lang/miri) instead. \
However, if Miri needs adjusting for rustc changes, just ignore this message.
"""
cc = ["@rust-lang/miri"]

Expand Down
Loading