Re: Why info files need to be named info-*.gz?

[Jörg Sommer <joerg@alea.gnuu.de>]

Hello Russ,

Russ Allbery <rra@debian.org> wrote:
> Jörg Sommer <joerg@alea.gnuu.de> writes:
>
>> the linitan warning info-document-has-wrong-extension refers to Policy
>> 12.2, but I can not find anything about the name scheme in this section.
>> Where is said, that a file in /usr/share/info must be named info*.gz?
>
> Policy says that they should be compressed with gzip -9.  If they're
> compressed but don't end in .gz, wouldn't lots of stuff break?

They are compressed and end in .gz.

% ls /usr/share/info/jed.*
/usr/share/info/jed.1in.gz  /usr/share/info/jed.3in.gz
/usr/share/info/jed.2in.gz  /usr/share/info/jed.info.gz

The lintian check looks so:
    unless ($infoext && $infoext =~ /info(-\d)?/) { # it's not foo.info
        unless (!@fname_pieces) { # it's not foo{,-{1,2,3,...}}
            tag "info-document-has-wrong-extension", "$file";
        }
    }

Bye, Jörg.
-- 
Wir leben zwar unter dem gleichen Himmel,
müssen aber nicht zwangsläufig den gleichen Horizont haben.