as you might already aware of, github is experiencing some problems today[0]. because its webhook is paused, our jenkins is not notified on "git push". as a result, PRs are not "make check" verified at this moment, and "git push" to ceph-ci does not trigger builds. let's keep an eye on [0], and hope they will it get back to normal soon. --- [0] https://status.github.com/messages -- Regards Kefu Chai
