On Thu, 17 Dec 2020 12:36:14 GMT, Aleksey Shipilev <shade at openjdk.org> wrote: > This looks like a cleanup and not very time-pressing, right? I'll take a look after NY holidays. Yes, just a small change. Take your time. ------------- PR: https://git.openjdk.java.net/jdk/pull/1745