On Mon, 20 Nov 2023 16:38:54 GMT, Magnus Ihse Bursie <ihse at openjdk.org> wrote: > Build change trivially okay Thanks Magnus! ------------- PR Comment: https://git.openjdk.org/jdk/pull/16719#issuecomment-1819529895