being confused with '5.10'. Arguably this is a PHP bug, but we need to work-around it for now, anyway.