[MariaDB developers] Re: 132c56f1325: online alter: extract the source to a separate file