Re: info handling dir.gz

[Lluís]

Glenn Morris writes:

> Thien-Thi Nguyen wrote:
>> +                   ;; As of 2011 or thereabouts, some weirdness in the
>> +                   ;; transition from Debian to GNU install-info results
>> +                   ;; in the directory file being gzipped.  Sigh.

> It's probably a bug in some package you have installed.
> See eg http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=537835
> I don't have a dir.gz on my Debian testing system.

I too have a /usr/share/info/dir.gz file. That probably explains why the info
directory has been so empty lately :)

Reinstalling a random package removes /usr/share/info/dir and regenerates
/usr/share/info/dir.gz.

So, I'd say it's necessary to install this patch. Besides, support for gzipped
dir files in install-info has been there there since version 4.0 (sep 1999), so
this patch can only make the handling more complete.


Lluis

-- 
 "And it's much the same thing with knowledge, for whenever you learn
 something new, the whole world becomes that much richer."
 -- The Princess of Pure Reason, as told by Norton Juster in The Phantom
 Tollbooth