Re: Unused OPTIONS variable in configure.in