Github PR label automation

[Kurt Roeckx]

On Sat, Feb 08, 2020 at 03:56:19PM +0000, Mark J Cox wrote:
> So right now here's what it does:
> 
> Every hour it looks at open PRs that are labelled "approval: done".
> If 24 hours has elapsed since that label was assigned and if there
> have been no comments made to the PR since the label was assigned then
> it is automatically moved to "approval: ready to merge" with a comment
> added to trigger notifications.  So if you want to stop something
> going to "ready to merge" just add any comment to the PR.

Does it also check that the CI says that everything is OK?