Re: Boxes not boxed in the header-line

[Richard Stallman]

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