diff options
| -rw-r--r-- | src/tools/miri/triagebot.toml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/tools/miri/triagebot.toml b/src/tools/miri/triagebot.toml index 5d6b596ea54..910e5f56e1e 100644 --- a/src/tools/miri/triagebot.toml +++ b/src/tools/miri/triagebot.toml @@ -50,8 +50,11 @@ new_pr = true [autolabel."S-waiting-on-author"] new_draft = true -# Canonicalize issue numbers to avoid closing the wrong issue when upstreaming this subtree +# Canonicalize issue numbers to avoid closing the wrong issue when upstreaming this subtree. [canonicalize-issue-links] -# Prevents mentions in commits to avoid users being spammed +# Prevents mentions in commits to avoid users being spammed. [no-mentions] + +# Show range-diff links on force pushes. +[range-diff] |