On Wed, 5 Apr 2023 01:48:19 GMT, David Holmes <dholmes at openjdk.org> wrote: > Renamings look good to me. Thank you for your review! ------------- PR Comment: https://git.openjdk.org/jdk/pull/12923#issuecomment-1497209787