IGNORECASE and index()

Hello,

In the info docs for Gawk 3.1.0 it says:

If  `IGNORECASE'  is  nonzero  or  non-null,  then  all string
comparisons and all  regular  expression  matching  are  case-
independent.  Thus, regexp matching with `~' and `!~', as well
as the `gensub', `gsub', `index', `match', `split', and  `sub'
functions,  record  termination with `RS', and field splitting
with `FS', all ignore case when doing their particular  regexp
operations.

I haven't tried the other operations listed here, but `index' is not
made case insensitive. Is the manual wrong, or is it a Gawk bug?

Hello,

In article <ckc1rp$1tp$1@reader08.wxs.nl>, Paul Boekholt wrote:
> In the info docs for Gawk 3.1.0 it says:
...
> I haven't tried the other operations listed here, but `index' is not
> made case insensitive. Is the manual wrong, or is it a Gawk bug?

$ gawk 'BEGIN{IGNORECASE=1; print index("BABA", "a")}'
2
$ gawk 'BEGIN{IGNORECASE=1; print index("BaBa", "A")}'
2
$ gawk --version
GNU Awk 3.1.3

Perhaps this was a bug in 3.1.0 which was fixed in newer versions.

Stepan Kasal