On Fri, 19 Jul 2024 10:42:00 GMT, Tobias Hartmann <thartm...@openjdk.org> wrote:
>> Can/should I include the bug number in some other way (perhaps directly in >> the comment)? I'm thinking if someone reads the comment in the future and >> would like more details. > > I don't think that's necessary, one can always find the changeset that added > a specific line/comment via the git history. Fair enough, now removed. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/20237#discussion_r1684254758
