Hi, at the moment the pdf's could not be generated. Therefore the make target 'extra-mirror-files' does really nothing expect wasting time. I suggest to suspend this useless target, I myself don't know how to, because I guess this must be done on the build machine.
Friedhelm -- PHP Documentation Mailing List (http://www.php.net/) To unsubscribe, visit: http://www.php.net/unsub.php
