> > Could the real problem be that awk is being used instead of
> > ${AWK} (which differ on my system)?
> 
> quite possibly. does your work/ directory have a .tools/bin/awk
> symlink?

no, it does not. I had been thinking about whether it ought to be created, and
if so, why it is in fact not, or if not, how I could force that.

-- 
Georg Schwarz    http://home.pages.de/~schwarz/
 geos@epost.de     +49 177 8811442