Github PR label automation

[Dr. Matthias St. Pierre]

> -----Original Message-----
> From: openssl-project <openssl-project-bounces at openssl.org> On Behalf Of Mark J Cox
> Sent: Saturday, February 8, 2020 8:52 PM
> To: Dmitry Belyavsky <beldmit at gmail.com>
> Cc: openssl-project at openssl.org
> Subject: Re: Github PR label automation
> 
> Thanks Dmitry; I hope that the comment triggers notifications to the
> creator without mentioning them?  (let me know if you get something
> changed labels that doesn't)   Mark

In fact, it was my suggestion *not* to add personal mentions. Since anybody who has posted 
comments to the pull request (which includes the submitter and all reviewers) will be subscribed
to the pull request's thread, I think a general comment which addresses nobody specific (just like
our "ping" messages) is less intrusive.

Matthias