On Wed, 3 Dec 2025 11:58:46 GMT, Nizar Benalla <nbenalla at openjdk.org> wrote: > Small doc-only change, the HTML file should have been updated as part of 8372940 Thanks for the reviews ------------- PR Comment: https://git.openjdk.org/jdk/pull/28631#issuecomment-3607335506