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’.
A patch is attached.
Regards,
Takeshi Ideriha