AWKPATH and AWKLIBPATH: default values different from documentation (gawk 5.0.1)

[Jannick]

Hi,

the default values of AWKPATH and AWKLIBPATH are documented to be
/usr/local/share/awk and /usr/local/lib/gawk, resp. (gawk 5.0.1).  However
the paths .:/usr/share/awk and /usr/lib/gawk are compiled into gawk 5.0.1
(built with ./configure && make), i.e., the fragment /local is dropped from
the documented paths.

At least for AWKPATH I would expect the default value (without redefining
them in the environment) to contain a sub-directory of /usr/local where I
can put my private awk scripts kept separate from the general installation
for better maintenance of each of them.  Is that correct - or am I missing
something here?

Many thanks,
J.