OpenJDK 11 changed the default javadoc output HTML version to HTML 5
from HTML 4.01. It causes an error on building Open MPI configured
with `--enable-mpi-java` (default: disable). This fix is compatible
with older OpenJDK.
I don't know whether this problem exists with other vender's JDKs.
But this fix should be compatible with other JDKs because the new
syntax is used in other places in the same file.
Thanks to Siegmar Gross for the bug report.
Signed-off-by: KAWASHIMA Takahiro <t-kawashima@jp.fujitsu.com>
b491b454dc