Hi Martin, On Mon, Sep 09, 2019 at 03:04:20PM +0200, Martin Liška wrote: > I'm suggesting to rename Deprecated to IgnoreWarn
That is an even worse name IMO. Just call it Removed or Deleted or something like that? Something that says what it _is_, not something that is an amalgamate of how we should handle it. Segher
