[Maria-discuss] MariaDB 10.4: subtle change of result ordering