My bug was actually related to that report: when I removed /usr/local/bin from root's PATH, the right install-info (/usr/bin/install-info) has been called, no longer /usr/local/bin's. Nevertheless, I would like to stress the fact that /usr/local/bin was *after* /usr/sbin in root's path!!! So it appears, somewhere, some way, $PATH is honored, but in a wrong order!!!! Akim