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 $ ls --si -l elisp.?? -rw-rw-r-- 1 g g 336k Sep 25 11:22 elisp.fn -rw-rw-r-- 1 g g 49 Sep 25 11:22 elisp.tp $ time TEXINDEX_AWK=/usr/bin/gawk texindex elisp.?? real 0m1.708s user 0m1.672s sys 0m0.009s $ time TEXINDEX_AWK=/usr/bin/mawk texindex elisp.?? real 0m0.610s user 0m0.591s sys 0m0.009s texindex can run two or more times when texi2pdf runs, so making it faster makes running texi2pdf more pleasant, meaning that you are more likely to run texi2pdf, and work on Texinfo documentation in general, so an all-round benefit to everyone.
