On Fri, 24 Jun 2022 10:54:06 GMT, Boris Ulasevich <bulasevich at openjdk.org> wrote: > You are right. Will the change be automatically pushed to the openjdk/jdk repo? Should I close this PR? Yes and yes. ------------- PR: https://git.openjdk.org/jdk/pull/9258