On Wed, 3 Dec 2025 20:37:25 GMT, Andrew Haley <[email protected]> wrote:
> https://github.com/openjdk/jdk/pull/28366/files?w=1 makes this PR easier to > read. Yes, "hide widespaces" is useful. Github is still surprisingly bad at managing large patches. ------------- PR Comment: https://git.openjdk.org/jdk/pull/28366#issuecomment-3610611623
