Re: Info-use-header-line

[Stefan Monnier]

>> Header lines may be set by minor modes and not just the major mode being
>> implemented.  An example is tabbar.
>> Is it a good idea to hide the header line if the user chooses to not
>> display a header line in a mode?  I think not.
>> 
>> A really good solution would, by the way, show global and local header
>> lines, but I think there's only one header line allowed at this point.

> There is a special buffer-local mode tabbar-local-mode, but it requires
> explicit enabling in every Info buffer.  So I agree that a simpler
> solution is to not overwrite the global value of the header line at all
> when Info-use-header-line is nil as implemented in your patch.

There's indeed a conflict between several possible uses of header-lines.
I'm not sure what we should about it in general.  In this specific case,
leaving the header-line alone sounds like a good idea: it doesn't solve
the problem, but allows the user to work around it.


        Stefan