I had no idea about your PR Mark. It's pity to see that many improvements (even simple) like this eventually was not implemented, despite the effort authors put into.
I have created PR with the change. https://github.com/php/php-src/pull/12056 If you think I should proceed with RFC please let me know. Of course it will not be merged into the PHP 8.3, but the next version. Kind regards, Jorg
