RFR: JDK-8295914: Add a header to generated HTML files in specs

[Erik Joelsson]

On Thu, 27 Oct 2022 20:50:04 GMT, Jonathan Gibbons <jjg at openjdk.org> wrote:

> Please review some updates to the parts of the build system related to building the documentation.

Build changes look fine in general.

make/Docs.gmk line 598:

> 596:   # Unset the following to suppress the link to the tool guides
> 597:   NAV_LINK_GUIDES = --nav-link-guides
> 598:   HEADER_RIGHT_SIDE_INFO = '<strong>$(subst &,&,$(JDK_SHORT_NAME))$(DRAFT_MARKER_STR)</strong>'

I think these assignments should just be `:=` unless you specifically need them to be lazy evaluated. We avoid the `=` lazy evaluation unless we specifically need it. I don't see a reason for that to be needed here though. Both JDK_SHORT_NAME and DRAFT_MARKER_STR are defined when these lines are reached.

-------------

PR: https://git.openjdk.org/jdk/pull/10891