Having mistakenly cloned php-src/php https://github.com/php-src/php
instead of php/php-src https://github.com/php/php-src (again), I figured
I'd ask -- is php-src used for anything?
The code seems to be quite old, and the content of php-src/php-src.github.io
https://github.com/php-src/php-src.github.io is a music video. Neither
seems productive to the PHP community.
Am I missing something?