On Tue, 27 Apr 2021 09:37:29 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: > That's a nice enhancement, looks good to me! Thanks for reviewing, Tobias! ------------- PR: https://git.openjdk.java.net/jdk/pull/3654