On Fri, 8 Aug 2025 16:28:15 GMT, Quan Anh Mai <qa...@openjdk.org> wrote:
>> `distinct()` has some overhead, do we need it? Do we expect duplicate >> headers in a file? > > It's not like stream is the most performant method to do anything anyway. I > think the clarification is worth the additional overhead, especially when > this file is not run very frequently. 3116b39c5dc812c1bfb0994bda3a82c9f66870af ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/26681#discussion_r2264028292