On Tue, 28 May 2024 18:57:07 GMT, Jonathan Gibbons <j...@openjdk.org> wrote:
> OK. I was just trying to honor the apparent intent to make the comment stand > out more than just a plain `//` comment, but I have no strong feelings > against reducing `///` to `//` In this case I would reduce it to '//' but others will have different opinions of course. ------------- PR Comment: https://git.openjdk.org/jdk/pull/19130#issuecomment-2136012355
