The first message of a pull request is copied into the merge commit when
bors/homu merges it. When a commit with an @-mention in the message is
pushed to any branch, GitHub sends an email notification to that person
(unless they have disabled email notifications).
Servo commits tend to be pushed multiple times: first in a PR’s branch,
then to master in servo/servo, then replicated into mozilla/gecko-dev,
and sometimes also replicated in other Mozilla repositories. This causes
as many unnecessary emails to be sent.
So if you want to attract someone’s attention, including to ask for
review, please do so in a subsequent comment on a pull request, not in a
commit message or initial pull request message.
Thanks!
--
Simon Sapin
_______________________________________________
dev-servo mailing list
dev-servo@lists.mozilla.org
https://lists.mozilla.org/listinfo/dev-servo
