[Maria-developers] [Branch ~maria-captains/maria/5.1-converting] Rev 2860: Automerge MariaDB 5.1.47 release into main.