On Thu, 4 Apr 2024 12:13:21 GMT, Roman Kennke <rken...@openjdk.org> wrote:
>> I think it is an old-style TODO. I'm considering if we shouldn't just remove >> these comments. What do people think about that? > > I'm not even sure what they want to say, really. Should be good to remove, > and if anybody can make sense of it, record an issue in the bug-tracker? OK. I removed the %%%. I'll wait a little bit to see if someone else wants to keep them for some reason, if not, I'll remove them. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/18618#discussion_r1551568127
