bug#41401: closed (27.0.91; gdb-mi headers use mode-line faces)

[GNU bug Tracking System]

Your message dated Tue, 19 May 2020 17:29:34 +0300
with message-id <address@hidden>
and subject line Re: bug#41401: 27.0.91; gdb-mi headers use mode-line faces
has caused the debbugs.gnu.org bug report #41401,
regarding 27.0.91; gdb-mi headers use mode-line faces
to be marked as done.

(If you believe you have received this mail in error, please contact
address@hidden.)


-- 
41401: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=41401
GNU Bug Tracking System
Contact address@hidden with problems
> --- Begin Message ---
>
>
>
> Subject: 
>
> 27.0.91; gdb-mi headers use mode-line faces
>
>
>
>
> Date: 
>
> Tue, 19 May 2020 14:43:34 +0200
>
>
>
>
> User-agent: 
>
> Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.8.0
>
>
>
>
> In gdb-mi, the formats used for header-line-format make use of the
> mode-line, mode-line-inactive and mode-line-highlight faces. This makes
> my headers misaligned since I customized the mode-line and
> mode-line-inactive faces to be narrower than the default face. (Changing
> the mode-line faces is also done in some themes inside etc/themes.)
>
> Maybe a good compromise would be to create new faces which inherit the
> mode-line faces by default, so at least there is an easy way to
> customize these new faces to fix the alignment.
>
>
>
>
> --- End Message ---
> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: bug#41401: 27.0.91; gdb-mi headers use mode-line faces
>
>
>
>
> Date: 
>
> Tue, 19 May 2020 17:29:34 +0300
>
>
>
>
> > From: Trevor Spiteri <address@hidden>
> > Date: Tue, 19 May 2020 14:50:29 +0200
> > 
> > This report can be closed.
>
> Done, thanks.
>
>
> --- End Message ---