Hi Ludo, >> Next, I replaced this line by >> >> AWK = /gnu/store/2kgp5d4wh40b49gp4qwqh2b4il29gq6g-profile/bin/gawk >> >> and re-ran "make install". Success! > > Could it be that there was a cache file here (‘config.cache’, as created > by “./configure -C”)? There is no config.cache, and I never used -C. Plus I do "make distclean" all the time. > In that case > > should be helpful if you haven’t seen it already! Just did. Looks like what I need. Thanks, Konrad.