Patrick Welche <prlw1(at)newn(dot)cam(dot)ac(dot)uk> writes:
> seems to actively want to get rid of those files (?!) Anyway, they are
> definitely not installed on my system. So, have things changed and the
> documentation lagged, or should those include files be installed?
"make install" doesn't install headers for server-side development.
Do "make install-all-headers" if you want the full include tree.
regards, tom lane