bug#27574: 25.2; `Info-use-header-line' documentation

[Drew Adams]

> > The doc should say that toggling the value has no effect if Info has
> > already been opened.  It's not even enough to quit Info.  Apparently
> you
> > must kill any `Info-mode' buffers and then open Info again, to see
> the
> > change.  This is not obvious.
> 
> This doesn't seem to be the case on the trunk, at least -- following
> any
> link in the Info buffer then gives you a display that respects this
> variable.
> 
> I think that's acceptable, and doesn't need clarification in the
> variable doc string.

Yes, and no.

The behavior is correct now, in the sense that the
header line is no longer used by Info.

But there is still/now a bug that the header line
is still present.  The bug report is still correct
that to get rid of it you need to kill Info buffers
and reopen Info.

IOW, the bug is almost fixed - the important failure
has been fixed.  A residual problem is that if you
change the option value we do not remove the (now
empty, no longer used for Info) header line from
existing Info buffers.

Using `q' to quit Info does not kill the buffer
(thank goodness).  Changing the value of this option
to turn it off should actually remove the header
line.  Info "not using" a header line means a bit
more than just not using it for Info purposes
(navigation etc.).  It should mean that Info uses
a header line.  If the option is off then Info
buffers should not have a header line.

---

On the other hand, to be really clear, they should
not use a header line created for Info.  Ideally,
we should keep track of whether a given header line
was created for/by Info, and remove only that when
the option is turned off.

IOW, some other code/library could add its own
header line (there can even be more than one, IIRC).
Ideally, Info should not just remove _a_ header
line.  It should remove a header line that it
created.

---

In any case, most of this bug has been fixed.
The problem that remains is minor compared to the
problem that existed.