Github PR label automation

[Mark J Cox]

Correct, it has no way to know if something has been put into ready to
merge deliberately despite it failing checks etc so it won't mess with
removing the label.

Mark

On Wed, Feb 12, 2020 at 10:39 AM Dr. Matthias St. Pierre
<Matthias.St.Pierre at ncp-e.com> wrote:
>
> > 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).
>
> If the does not automatically remove the "ready to merge" label, but only
> refrains from setting it automatically, that's a good compromise I can live with.
>
> Matthias
>