[PD-dev] Patch to fix up man page installation under Linux.