[phpMyAdmin Developers] Jenkins

Hi all [Resending as apparently it didn't reach most of you due to Gmail rejecting my mails.] For quite some time we're using Jenkins for CI. We've also added Travis during next the years. Do you think it's reasonable to still have both of them? Own Jenkins server requires some maintenance and currently doesn't integrate that well with GitHub as Travis. This could be probably addressed, but the questions is whether it's worth of it. My personal opinion is that Jenkins does not really have any benefits, so maybe it's time to drop it from our infrastructure. PS: I've disabled error-reporting-server tests there as they are apparently failing due to some timezone errors. -- Michal Čihař | https://cihar.com/ | https://weblate.org/