On Thu, 4 May 2023 21:24:45 GMT, Jonathan Gibbons <jjg at openjdk.org> wrote: > The true source of the man page is upstream in an internal repo. Ah, got it - thanks for the heads-up. Not my problem then :) ------------- PR Comment: https://git.openjdk.org/jdk/pull/13332#issuecomment-1535444786