Re: master ec9523a: Add a keybinding to the help menu to display manuals

[Lars Ingebrigtsen]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

>> files under info/ end in ".info".  Are there known cases of
>> extensionless info files that do not correspond to a file ending in
>> ".info" or ".info.gz" (or another compression suffix)?  If not, then
>> removing that bit of the code will prevent the current false positives.
>
> It used to be common to have Info files with names like `foo`, `foo-1`,
> `foo-2`, ...  Splitting Info files has gotten out of fashion due to the
> growing size of RAM, and the use of a `.info` extension has grown
> a lot too.  Maybe we could start assuming that all those files nowadays
> have a `.info` extension?

I had a look in

/usr/share/info/

here, and it looks like they all have .info in their names.

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no