Re: [bug-gawk] awk_ext_id_t inconsistency

[Andrew J. Schorr]

Thanks. I'm cc'ing bug-gawk so "everybody" will know...

On Thu, Jan 11, 2018 at 09:24:32PM +0100, Antonio Giovanni Colombo wrote:
> Hi everybody,
> 
> I will take care of the Italian part...
> 
> All the best, Antonio
> 
> 
> On Thu, Jan 11, 2018 at 9:22 PM, Andrew J. Schorr <
> address@hidden> wrote:
> 
> > Hi,
> >
> > On Thu, Jan 11, 2018 at 09:55:46PM +0200, Arnold Robbins wrote:
> > > I have fixed this and will push it out to the repo. Much thanks
> > > for the report and discussion.
> >
> > Thanks for cleaning this up. I think you may have missed a few spots:
> >
> > bash-4.2$ git grep -n 'awk_ext_id_t *\*' | cat -
> > doc/it/gawktexi.in:36716:static awk_ext_id_t *ext_id;
> > doc/it/gawktexi.in:37487:static awk_ext_id_t *ext_id;
> > gawkapi.h:950:             awk_ext_id_t *ext_id,        /* ditto */
> > gawkapi.h:980:        awk_ext_id_t *ext_id,     /* ditto */
> >
> > Regards,
> > Andy
> >
> >
> 
> 
> -- 
>    /||\    | Antonio Colombo
>   / || \   |  address@hidden
>  /  ()  \  | address@hidden
> (___||___) |   address@hidden