On Fri, 19 May 2023 10:50:39 GMT, Alan Bateman <alanb at openjdk.org> wrote: > > May I push it now since it's a build breakage? Thanks. > > Yes, the change is trivial so please go ahead. Thanks @AlanBateman . ------------- PR Comment: https://git.openjdk.org/jdk/pull/14057#issuecomment-1554418471