Remove duplicate "./configure --help" output; fixes #4075