Dear Peter,
> > Description: server includes not installed by default
>
> make install-all-headers
Good, but not enough?
I still argue that it should be done "by default", so that "extensions"
can be sure to find it. You cannot ask for the installer to reinstall if
s?he forgot it...
--
Fabien Coelho - coelho@cri.ensmp.fr