Re: Boxes not boxed in the header-line

[Stefan Monnier]

>     I just noticed this inelegant behavior: in the header-line, when two
>     pieces of text have different box settings (but they're both 3d
>     boxes), the top and bottom part of the two texts are correctly drawn
>     (with their respective 3D effect), but there is not vertical line
>     between the two to mark the transition from one to the other.

> Is it really meaningful to have one box immediately after another
> with no space between?  Maybe the right solution is to say "so don't
> do that, then".

Notice that in my example, every box is indeed separated from the next one
by a space, but the whole header line is itself marked as boxed by the
header-line face so the separating space is "boxed" as well,
tho differently (e.g. different thickness).


        Stefan