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

[Eli Zaretskii]

On Sat, 8 Dec 2001, Anthony DeRobertis wrote:

> 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. 

I think the changes I sent make the above work correctly, at least
most of the time, even though they don't actually _force_ a
case-sensitive search (which is almost impossible to do without
rewriting lots of code).

So I suggest that you run with the modified Info for a while and see
if it does what you want.  If you see something that still doesn't
work as you think it should, please come back and report that case
here.