On Thu, 30 Mar 2023 14:19:55 GMT, Eirik Bjorsnos <d...@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

Reply via email to