[review v2] Add TUI border colors

[Eli Zaretskii]

> Date: Fri, 22 Nov 2019 18:54:13 -0500
> From: "Tom Tromey (Code Review)" <gerrit@gnutoolchain-gerrit.osci.io>
> 
> +@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 wonder if we could say the "Note" part only once, for both
tui-border and tui-active-border.  It sounds redundant to repeat the
same text so close to one another.

Otherwise, the documentation parts are OK.  Thanks.