Re: [PATCH] Document style behavior in batch mode.

[Eli Zaretskii <eliz@gnu.org>]

> From: Alan Hayward <Alan.Hayward@arm.com>
> CC: nd <nd@arm.com>, Alan Hayward <Alan.Hayward@arm.com>
> Date: Thu, 21 Feb 2019 13:23:44 +0000
> 
> Style is disabled when running in batch mode.
> 
> gdb/ChangeLog:
> 
> 2019-02-21  Alan Hayward  <alan.hayward@arm.com>
> 
> 	* NEWS: Update style defaults.
> 
> gdb/doc/ChangeLog:
> 
> 2019-02-21  Alan Hayward  <alan.hayward@arm.com>
> 
> 	* gdb.texinfo: Update style defaults.

This is OK, but:

> --- a/gdb/doc/gdb.texinfo
> +++ b/gdb/doc/gdb.texinfo
> @@ -24514,8 +24514,9 @@ Show the current pagination mode.
>  @kindex set style
>  @kindex show style
>  @value{GDBN} can style its output on a capable terminal.  This is
> -enabled by default on most systems.  Various style settings are
> -available; and styles can also be disabled entirely.
> +enabled by default on most systems, but disabled by default when in
> +batch mode.  Various style settings are available; and styles can
> +also be disabled entirely.

Please insert "(@pxref{Mode Options})" (without the quotes) after
"batch mode", to provide the readers of the manual with a hyperlink to
where that mode is described.

Thanks.