Hello, this is my first posting to the mailing list.
It seems that the description of message displayed after running ‘make world’ is
different from the actual message echoed on a terminal.
Actually, GNUmakefile.in says ‘~ documentation successfully made’
but the documentation says ‘~ html documentation successfully made’.
https://github.com/postgres/postgres/blob/master/GNUmakefile.in <https://github.com/postgres/postgres/blob/master/GNUmakefile.in>
A patch is attached.
Regards,
Takeshi Ideriha