Indeed. I should also note that the issue reported at https://phabricator.wikimedia.org/T280064 is about xdebug not being found. I don't have an explanation for this; perhaps something was missed while switching the job to PHP 7.3. OTOH, my proposed solution will make it possible to use pcov instead of xdebug, thus basically ignoring the current issue with xdebug. The rationale being, I don't think it's necessary to unbreak xdebug support if we're migrating away from it anyway.