[MariaDB developers] Re: CI failures visible on GitHub (affecting contributors)