Ensure that mysql_get_server_version() also works if there is a non numerical prefix before the version number