Re: Boxes not boxed in the header-line

[Richard Stallman]

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

Is that really a reasonable thing to do?  It sounds nonsensical to me,
and if it is nonsensical, we need not spend time trying to make it "work".