diff options
| author | bors <bors@rust-lang.org> | 2024-09-17 07:00:09 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-09-17 07:00:09 +0000 |
| commit | 9c3a392348c7171a51a7d42a4f5a817c64459845 (patch) | |
| tree | 225b42e24976372d60f582ccda84f6943e4b5562 | |
| parent | f6ae3cb0fb4079813712f90dbb22515274d289f6 (diff) | |
| parent | e04dc624a708aec084b6817d44261e00d0d70c2c (diff) | |
| download | rust-9c3a392348c7171a51a7d42a4f5a817c64459845.tar.gz rust-9c3a392348c7171a51a7d42a4f5a817c64459845.zip | |
Auto merge of #3893 - rust-lang:autolabel, r=RalfJung
Automatically add/remove labels when github review (requests) are used
| -rw-r--r-- | src/tools/miri/triagebot.toml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/tools/miri/triagebot.toml b/src/tools/miri/triagebot.toml index addb36418d4..2d93777f61d 100644 --- a/src/tools/miri/triagebot.toml +++ b/src/tools/miri/triagebot.toml @@ -17,3 +17,15 @@ contributing_url = "https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.m [no-merges] exclude_titles = ["Rustup"] + +[review-submitted] +# This label is added when a "request changes" review is submitted. +reviewed_label = "S-waiting-on-author" +# These labels are removed when a "request changes" review is submitted. +review_labels = ["S-waiting-on-review"] + +[review-requested] +# Those labels are removed when PR author requests a review from an assignee +remove_labels = ["S-waiting-on-author"] +# Those labels are added when PR author requests a review from an assignee +add_labels = ["S-waiting-on-review"] |