On Mon, 17 Dec 2018, Patrick Donnelly wrote: > This PR check has been failing a lot recently for months and, with > recent policy changes, this makes it difficult to merge PRs. Can we > make this check optional somehow or just turn it off? Note that it is already optional--you can still merge when it fails. That doesn't it make it less annoying/useless, though, since the red X obscures other failures on the list views. sage
