Re: address@hidden: Bug#122594: info: Index isn't sure if it should be case sensitive or not]

[Anthony DeRobertis]

Eli Zaretskii writes: 

> Do the two changes below, applied one after the other, help solve
> this problem?

I don't think so, unless I fudged the build up. I did an apt-get source, 
patch -p0, then dpkg-buildpackage -rfakeroot -b. Naturally, the signing 
failed. BTW: Both patches applied with an offset of -3. 

I then did dpkg -i on the resulting deb. After doing that, info still gives 
the weird behavior for YYER<tab> turning into yyerro instead of either 
YYERRO or YYERROR. 

> For example, there
> are manuals where all index entries begin with a capital letter;
> users shouldn't be expected to know that.

Well, if the user typed in "inde" it wouldn't matter if the info author used 
"INDEX" instead of "index"; lowercase matches anything. Only if the user 
typed in something with uppercase would it matter, but that's arguably a bug 
with the documentation if the case on, e.g., C identifiers is wrong. 

Or at least my C compiler thinks its a bug when I use the wrong case for 
identifiers ;-)