Re: [RFC 8.3 2/3] Add the "set style source" command

[Philippe Waroquiers <philippe dot waroquiers at skynet dot be>]

On Fri, 2019-03-08 at 14:04 -0700, Tom Tromey wrote:
> diff --git a/gdb/NEWS b/gdb/NEWS
> index cc7c35c0642..06564311643 100644
> --- a/gdb/NEWS
> +++ b/gdb/NEWS
> @@ -145,6 +145,12 @@ show style enabled
>    Enable or disable terminal styling.  Styling is enabled by default
>    on most hosts, but disabled by default when in batch mode.
>  
> +set style sources [on|off]
> +show style sources
> +  Enable or disable source code styling.  Source code styling is
> +  enabled by default, but only takes effect if styling in general is
> +  enabled, if if GDB was linked with GNU Source Highlight.
As already reported by Eli : if if -> and if ?

Also, this NEWS entry explains that 'on' takes effect only
if styling is on, but neither the help nor the user manual
are explaining this.
Maybe the help and/or user manual should also explain this ?

Thanks

Philippe