php-src Git hash abbreviation collisions

Hi all, I've just noticed a pull request[1] which suggests to no longer abbreviate the php-src Git hashes to 7 digits only, because there are already collisions. Using 10 digits as suggested seems reasonable to me, but I wanted to check if there are other places affected than the RM tools. So, is anybody aware of some of our tooling also using 7 digit hash abbreviations? Do we need to announce that change elsewhere than besides on <https://windows.php.net/>? [1] <https://github.com/php/web-rmtools/pull/15> Christoph