doc: Fixes mentions of mention-bot.

Its last mention was on 2017-09-25. Close to a year.

The CODEOWNERS feature of github, though, fills in the gap in a more
appropriate manner (IMHO).
This commit is contained in:
Samuel Dionne-Riel 2018-08-05 20:19:46 -04:00
parent 2428f5dda1
commit e97112bdc3

View File

@ -103,8 +103,9 @@
<itemizedlist> <itemizedlist>
<listitem> <listitem>
<para> <para>
mention-bot usually notifies GitHub users based on the submitted changes, <link xlink:href="https://help.github.com/articles/about-codeowners/">CODEOWNERS</link>
but it can happen that it misses some of the package maintainers. will make GitHub notify users based on the submitted changes, but it can
happen that it misses some of the package maintainers.
</para> </para>
</listitem> </listitem>
</itemizedlist> </itemizedlist>
@ -376,8 +377,9 @@ $ nix-shell -p nox --run "nox-review -k pr PRNUMBER"
<itemizedlist> <itemizedlist>
<listitem> <listitem>
<para> <para>
Mention-bot notify GitHub users based on the submitted changes, but it <link xlink:href="https://help.github.com/articles/about-codeowners/">CODEOWNERS</link>
can happen that it miss some of the package maintainers. will make GitHub notify users based on the submitted changes, but it can
happen that it misses some of the package maintainers.
</para> </para>
</listitem> </listitem>
</itemizedlist> </itemizedlist>