> I have made this change in commit 5661fc4c01b (today). (It was not
> as hard as I expected as I just bypassed the code in \pdfgettoks,
> which is kind of a black box to me.)
Thanks!
> I'm afraid this is really not possible at the moment. A single
> index entry could even have multiple page numbers for different
> locations in the manual. It would require changes to the index
> files and texindex, and possibly texi2dvi as well. We are already
> making a relatively small change to the index file format in the
> next release (changing from \ to @ as the escape character), which
> change has not been without difficulties.
OK, no problem. It was just an item of a wishlist :-)
Werner