On Tue, 7 May 2024 11:53:19 GMT, Pavel Rappo <pra...@openjdk.org> wrote:
> Please review this mechanical change to man pages. This PR should be > integrated after https://github.com/openjdk/jdk/pull/18787. Thanks for reviewing it Joe, I'm now delegating integration of this PR to @JesperIRL, you, or anyone who will be integrating https://github.com/openjdk/jdk/pull/18787. ------------- PR Comment: https://git.openjdk.org/jdk/pull/19119#issuecomment-2099395990
