On Tue, 29 Aug 2023 10:45:30 GMT, Andrew Dinn <adinn at openjdk.org> wrote: > Nice work. Many thanks, @adinn! I massaged in your feedback. ------------- PR Comment: https://git.openjdk.org/jdk/pull/15041#issuecomment-1697492382