On Mon, 7 Feb 2022 16:22:25 GMT, Goetz Lindenmaier <goetz at openjdk.org> wrote: >> ...like in the new commit. > > Good point to rename this! Oh, ok, reading the option description helps. ------------- PR: https://git.openjdk.java.net/jdk/pull/7362