github allow "merge" PR even CI is not finished

[asroy]

For some reason, if CI passed previously for a old commit, github will allow "merge" option, even new CI of new commit is not finished.

[illsilin]

I think this is no longer an issue. Our CI is pretty stable now and sometimes we feel confident enough to merge PRs without waiting for CI to finish.