Re: header-line and mode-line faces

[Stefan Monnier]

>> > They are different faces, and you can also customize them 
>> > separately. But header-line inherits from mode-line *today*. Why?
>> 
>> So that it can share some of its attributes.  E.g. if you change the
>> font-family or the size of the mode-line it'll change the 
>> corresponding attribute of the header-line as well.

> Exactly.

> I am suggesting that, by default, it share all of its attributes. That's all.

Yes, we got your point.  We just don't agree.


        Stefan