On 08/13/2018 02:14 AM, Paul Eggert wrote:
> Ulrich Mueller wrote:
>> Maybe it would be cleaner to call the option --with-gmp (and invert its
>> logic), after all? It could still be enabled by default.
>
> Works for me.
>
On further thought it's probably a bit clearer to call it --with-libgmp 
rather than --with-gmp since GMP code is always used one way or another, 
so I installed the attached.