> From: Gavin Smith <[email protected]> > Date: Mon, 24 Oct 2022 18:01:21 +0100 > Cc: [email protected], [email protected] > > On Mon, Oct 24, 2022 at 06:40:53PM +0300, Eli Zaretskii wrote: > > Why not prefer Gawk if it's installed? > > It makes running texi2pdf a little faster. > > $ ls -l --si texinfo.?? > -rw-rw-r-- 1 g g 94k Oct 24 17:51 texinfo.cp > -rw-rw-r-- 1 g g 21k Oct 24 17:51 texinfo.fn > $ time TEXINDEX_AWK=/usr/bin/gawk texindex texinfo.?? > > real 0m0.459s > user 0m0.453s > sys 0m0.007s > $ time TEXINDEX_AWK=/usr/bin/mawk texindex texinfo.?? > > real 0m0.161s > user 0m0.156s > sys 0m0.006s
I'd leave this to local configurations, for people who really care about these differences. texindex was written by the Gawk developer and maintainer, so it really is suited best to Gawk, not to other Awks. These minor speedups aren't IMO worth the risk of breaking texindex. And I didn't even start talking about MS-Windows yet, where the fact that any other Awk works here is sheer luck, since AFAIK the other Awks don't have a Windows developer. My $0.02, anyway.
