On Tue, 21 Mar 2023 21:08:01 GMT, Jonathan Gibbons <[email protected]> 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 <[email protected]> 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
