On Tue, 28 May 2024 20:22:24 GMT, Jonathan Gibbons <j...@openjdk.org> wrote:
> What about changing `///` to `//---` to give slightly more prominence to > these comments, over plain old `//` comments. The dashes give a small sense > of a horizontal rule, to delimit sections of code. > > (FWIW, I have locally edited `//|` to `//` and such comments do not stand out > beside existing use of `//`.) `//---` seems okay, it would stand out a bit more. ------------- PR Comment: https://git.openjdk.org/jdk/pull/19130#issuecomment-2136060411