On Tue, 15 Jun 2021 15:35:14 GMT, Maurizio Cimadamore <[email protected]> wrote:
> I can push to 17 if desired, but I'll need a new PR for that pushing to 17 would be nice; the script is equally broken and unusable there. ------------- PR: https://git.openjdk.java.net/jdk/pull/4492
