Re: [review] Add TUI border colors

[Eli Zaretskii <eliz@gnu.org>]

> Date: Sun, 10 Nov 2019 11:40:39 -0500
> From: "Tom Tromey (Code Review)" <gerrit@gnutoolchain-gerrit.osci.io>
> 
> +TUI active border display styling.\n\
> +Configure TUI active border colors\n\
> +The \"tui-active-border\" style is used when GDB displays the border of a\n\
> +TUI window that does have the focus."), true);

Instead of "that does have the focus", I'd say "that has the focus".
I think the former builds on the doc string for tui-border, and is
less clear when read separately.

> +@item tui-border
> +Control the styling of the TUI border.  Note that, unlike other
> +styling options, only the color of the border can be controlled via
> +@code{set style}.  This was done for compatibility reasons, as TUI
> +controls to set the border's intensity predated the addition of
> +general styling to @value{GDBN}.  @xref{TUI Configuration}.
> +
> +@item tui-active-border
> +Control the styling of the active TUI border; that is, the TUI window
> +that has the focus.  Note that, unlike other styling options, only the
> +color of the border can be controlled via @code{set style}.  This was
> +done for compatibility reasons, as TUI controls to set the active
> +border's intensity predated the addition of general styling to
> +@value{GDBN}.  @xref{TUI Configuration}.

I'd suggest to have the note only once, for both options.

The documentation parts are OK with these nits fixed.

Thanks.