On Mon, 8 Jan 2024 09:21:56 GMT, Emanuel Peter <epeter at openjdk.org> wrote: > Yes, I think that would be preferrable, even though this is not a very complicated fix. Okay. Thanks. ------------- PR Comment: https://git.openjdk.org/jdk/pull/17190#issuecomment-1880655516