diff options
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 2 | ||||
| -rw-r--r-- | src/tools/miri/triagebot.toml | 11 |
2 files changed, 12 insertions, 1 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index fef7f807e93..e4302b734aa 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -13,7 +13,7 @@ for a list of Miri maintainers. [Rust Zulip]: https://rust-lang.zulipchat.com -### Pull review process +### PR review process When you get a review, please take care of the requested changes in new commits. Do not amend existing commits. Generally avoid force-pushing. The only time you should force push is when there diff --git a/src/tools/miri/triagebot.toml b/src/tools/miri/triagebot.toml index 60e80c3f673..c109b620846 100644 --- a/src/tools/miri/triagebot.toml +++ b/src/tools/miri/triagebot.toml @@ -17,6 +17,17 @@ allow-unauthenticated = [ [assign] warn_non_default_branch = true contributing_url = "https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.md" +[assign.custom_welcome_messages] +welcome-message = """ +Welcome, and thank you for contributing to Miri! +To ensure a smooth reviewing experience, please read https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.md#pr-review-process. +In particular, please do not force-push to the PR branch except when you need to rebase due to a conflict or when the reviewer asks you for it. +""" +welcome-message-no-reviewer = """ +Welcome, and thank you for contributing to Miri! +To ensure a smooth reviewing experience, please read https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.md#pr-review-process. +In particular, please do not force-push to the PR branch except when you need to rebase due to a conflict or when the reviewer asks you for it. +""" [no-merges] exclude_titles = ["Rustup"] |