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

Tue Nov 1 18:42:27 UTC 2022

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.

This pull request has now been integrated.

Changeset: d17bf51f
Author:    Jonathan Gibbons <jjg at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/d17bf51f91371072a758e775136af946192e771b
Stats:     144 lines in 3 files changed: 139 ins; 1 del; 4 mod

8295914: Add a header to generated HTML files in specs

Reviewed-by: erikj, iris

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

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