On Tue, 2 Mar 2021 09:09:36 GMT, Roland Westrelin <roland at openjdk.org> wrote: > Looks good to me Thanks @rwestrel for your review. Is it OK to be pushed? It's trivial, right? ------------- PR: https://git.openjdk.java.net/jdk/pull/2786