Alexandre Oliva writes: > The known workarounds are setting CONFIG_SHELL=/bin/ksh or wiping > out target_dir/config.cache. Oh. Fine then. Thanks! Please disregard the last comment I sent about it, and sorry about the noise. ./A