On Tue, Sep 10, 2019 at 05:46:14PM +0100, Richard Sandiford wrote:
> Jakub Jelinek <ja...@redhat.com> writes:
> > On Tue, Sep 10, 2019 at 06:14:11PM +0200, Martin Liška wrote:
> >> On 9/9/19 11:14 PM, Joseph Myers wrote:
> >> > On Mon, 9 Sep 2019, Jakub Jelinek wrote:
> >> >
> >> > > > "IgnoreWarn" reads as "ignore the warning".
> >> > > >
> >> > > > If we want it named as two things, can we just make it two things?
> >> > > > "Ignore WarnDeleted" or something. Which also says what it is
> >> > > > warning
> >> > > > about.
> >> > >
> >> > > Or WarnRemoved. Both work for me, but ultimately it would be best if
> >> > > Joseph
> >> > > decides.
> >> >
> >> > I prefer WarnRemoved.
> >> >
> >>
> >> Works for me. I'm going to install the tested patch.
> >
> > I thought the decision is to replace Deprecated with Ignore WarnRemoved
> > where Ignore would handle the ignoring and WarnRemoved just add the warning
> > part on top of it. So, OPT_SPECIAL_ignore plus some flag for WarnRemoved.
>
> Is there any time you'd use WarnRemoved without Ignore though?
No.
> Seems better not to require two flags when one would do.
Well, the idea was to make it clear what it does. That the current
Deprecated is about ignoring the option and on top of that warning
because the option has been removed.
It is more typing, but that is it, the *.awk scripts can diagnose easily
if WarnRemoved is used without Ignore.
Jakub
