Bors should remove mentions (`@<username>`) from PR descriptions, which are turned into merge commit bodies, to avoid spamming people on GitHub. See https://github.com/rust-lang/homu/pull/100 and https://github.com/rust-lang/homu/pull/230 for more details.