Stale PR stats @May01

[Mark J Cox]

On Fri, May 1, 2020 at 3:30 PM Dmitry Belyavsky <beldmit at gmail.com> wrote:
..
> And I also got an idea that ping comment leaves PRs out of this statistics :)

Thanks!  The script is designed to ignore the automated pings that it
creates itself so they themselves don't reset the dates and
artificially stop things being stale.  Instead they will hopefully
nudge folks into taking some action that will actually stop the PRs
being stale :))

Mark