On Tue, 15 Jun 2021 19:50:12 GMT, Erik Joelsson <erikj at openjdk.org> wrote: > This comment should now end up in ide-support-dev as well. Not really (at least for now) :-) ------------- PR: https://git.openjdk.java.net/jdk17/pull/61