On Tue, 19 Dec 2023 16:47:33 GMT, Goetz Lindenmaier <go...@openjdk.org> wrote:
> try it! I got the instructions to replicate in my local repo later, so wasn't sure to proceed. Thanks for the suggestion. I think this makes it easier to keep in sync with the other change. ------------- PR Comment: https://git.openjdk.org/jdk/pull/16604#issuecomment-1864127477