Re: awk for config headers

[Ralf Wildenhues]

* Paul Eggert wrote on Tue, Oct 09, 2007 at 12:17:45AM CEST:
> 
> Sorry, that's a bug in the manual; traditional Awk supported 'index'.
> I fixed it as described below.

Thanks!

> Ralf Wildenhues <address@hidden> writes:
> > If you can assert that `index' is safe to use, I'll apply the patch.
> 
> Please go ahead.

Done.  I'll address Benoit's remark about three-argument split and the
doc update in a followup patch.

Cheers,
Ralf