Hello, What is the recommended way of merging a PR when Travis-CI failed for unrelated reasons? (apparently an external NNTP server is having hiccups) See https://github.com/python/cpython/pull/4065 Regards Antoine.