[review v2] Add TUI border colors

[Tom Tromey]

>>>>> "Eli" == Eli Zaretskii <eliz@gnu.org> writes:

>> 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}.

Eli> I wonder if we could say the "Note" part only once, for both
Eli> tui-border and tui-active-border.  It sounds redundant to repeat the
Eli> same text so close to one another.

Eli> Otherwise, the documentation parts are OK.  Thanks.

Thanks.  I removed one of the notes.
I'm going to check this in shortly.

Tom