On May 7, 2018, at 15:35, Perry E. Metzger wrote: > On Mon, 7 May 2018 09:55:17 -0500 Ryan Schmidt wrote: >> When I submit a PR to add a maintainer's GitHub handle to their >> ports, I assign the ticket to them (if I can; if I can't, because >> they're not in the developer team, I @mention them in the >> description), and then I use [skip notification] so that they >> aren't notified about it a second time (once for the PR, once for >> the notification comment), and so that any other maintainers aren't >> bothered about the change. >> >> If the notification bot were a little smarter, and didn't do a >> notification if the only person to be notified is the person to >> whom the PR is already assigned, or from whom a review was already >> requested, that would help a little. > > Would you like the reminder on how to use "skip notification" > restored? I'd want to put it at the bottom though, so as not to > confuse average requesters.
I don't know. If you remove the documentation of this feature from the pull request template, will you document it elsewhere?
