Github PR label automation

[Mark J Cox]

I thought about it some more and Kurt is right.  Something shouldn't
be in "Ready to Merge" unless it's actually ready to merge.  For
example 10993.  This PR shouldn't be ever automatically moved to ready
to merge because it failed CI.  A human has determined it is ready to
merge and applied the label.  So "ready to merge" really ought to mean
that.  So I've updated the live script that's running to do that
check.  It will not move to 'ready to merge' state automatically
unless (or until) all CI passes.  (I'll do a PR for the tool with that
change shortly).

Mark

On Wed, Feb 12, 2020 at 8:49 AM Dr. Matthias St. Pierre
<Matthias.St.Pierre at ncp-e.com> wrote:
>
> > > Does it also check that the CI says that everything is OK?
> >
> > Do we want it to?  I assumed that Approval: done was not being applied
> > unless tests past (but looking that's not always the case). Can we
> > assume that something in "approval: ready to merge" but that failed CI
> > won't get merged?  Otherwise I could add a CI check on the move to
> > "ready to merge".
>
> It does not check and I don't think it should attempt to do it. The only task of
> this script should be to automatically promote the [approval: done] state to
> [approval: ready to merge] after the grace period has expired, because humans
> tend to forget that. Anything beyond that, in particular an attempt to judge
> whether the approval is valid or not, and whether a CI failure can be ignored or
> not, should be left to humans.
>
> Matthias
>