On Tue, 15 Jun 2021 15:35:14 GMT, Maurizio Cimadamore <mcimadam...@openjdk.org> 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
