On Fri, 19 May 2023 10:50:39 GMT, Alan Bateman <al...@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
