Add note about the various phpenv tools

doc/ci/languages/php.md

@@ -179,6 +179,14 @@ Using phpenv also allows to easily configure the PHP environment with:
 phpenv config-add my_config.ini
 ```
 
+*__Important note:__ It seems `phpenv/phpenv`
+ [is abandoned](https://github.com/phpenv/phpenv/issues/57). There is a fork
+ at [madumlao/phpenv](https://github.com/madumlao/phpenv) that tries to bring
+ the project back to life. [CHH/phpenv](https://github.com/CHH/phpenv) also
+ seems like a good alternative. Picking any of the mentioned tools will work
+ with the basic phpenv commands. Guiding you to choose the right phpenv is out
+ of the scope of this tutorial.*
+
 ### Install custom extensions
 
 Since this is a pretty bare installation of the PHP environment, you may need