Hey all, After a discussion on options in the leadership team today, I ticked a box in the Github interface that prevents repository administrators from merging PRs to master that don't pass status checks (ie, make check). Hopefully this was rare anyway, and what we've really done is added some security against accidental "git push" of test branches that aren't ready yet and being just that little bit more sure that we aren't breaking things for other people. But maybe this is going to be an issue for us – if you find yourself needing to override, you have the ability to turn it off (temporarily?) — please let me know if it causes you trouble! If it goes well I'll consult with the backports team and similarly check that box for our stable branches. -Greg
