[PATCH 3/4] gdb: add 'maint set/show gnu-source-highlight enabled' command

[Andrew Burgess]

* Eli Zaretskii via Gdb-patches <gdb-patches@sourceware.org> [2022-01-11 15:34:12 +0200]:

> > Date: Tue, 11 Jan 2022 13:07:44 +0000
> > From: Andrew Burgess <aburgess@redhat.com>
> > Cc: gdb-patches@sourceware.org
> > 
> >   @kindex maint set gnu-source-highlight enabled
> >   @kindex maint show gnu-source-highlight enabled
> >   @item maint set gnu-source-highlight enabled @r{[}on|off@r{]}
> >   @itemx maint show gnu-source-highlight enabled
> >   Control whether @value{GDBN} should use the GNU Source Highlight
> >   library for applying styling to source code (@pxref{Output Styling}).
> >   This will be @samp{on} by default if the GNU Source Highlight library
> >   is available.  If the GNU Source Highlight library is not available,
> >   then this will be @samp{off} by default, and attempting to change this
> >   value to @samp{on} will give an error.
> >   
> >   If the GNU Source Highlight library is not being used, then
> >   @value{GDBN} will use the Python Pygments package for source code
> >   styling, if it is available.
> >   
> >   This option is useful for debugging @value{GDBN}'s use of the Pygments
> >   library when @value{GDBN} is linked against the GNU Source Highlight
> >   library.
> > 
> > Is this better?
> 
> Yes, thanks.

Thanks, I pushed this patch.

Andrew