Integrated: JDK-8304689: Add hidden option to disable external spec page

Mon Mar 27 15:44:56 UTC 2023

On Tue, 21 Mar 2023 21:08:01 GMT, Jonathan Gibbons <jjg at openjdk.org> wrote:

> Please review a change to introduce a hidden option to temporarily disable the "External Specifications" page while we add `@spec` tags, and until we have a critical mass of such tags.

This pull request has now been integrated.

Changeset: 2f34687e
Author:    Jonathan Gibbons <jjg at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/2f34687ec1210317a9215496d0184fe30bda6437
Stats:     58 lines in 5 files changed: 47 ins; 0 del; 11 mod

8304689: Add hidden option to disable external spec page

Reviewed-by: erikj, hannesw

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

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