On Thu, 30 Mar 2023 14:19:55 GMT, Eirik Bjorsnos <duke at openjdk.org> wrote: > Is this repurposing of warn.flag.is.deprecated considered ok? yes, that's not used. It was a leftover from JDK-8204981 & JDK-8234596. ------------- PR Comment: https://git.openjdk.org/jdk/pull/13158#issuecomment-1490647633