Paul Eggert wrote: > Perhaps we could make "exec </dev/null" an option, normally enabled,
I'm sorry, I didn't follow this discussion closely. If I understand the shell docs correctly this command redirects stdin to /dev/null for all further lines of configure. Why would anybody want this? Andreas
