Re: [PATCH] gnu: gzochi: Update to 0.10.

[Andreas Enge]

Hello,

thanks for your contribution!

On Sun, Aug 21, 2016 at 11:20:54AM -0400, Julian Graham wrote:
> -              ("gmp" ,gmp)

Could you comment on this? Is it not needed any more? Or does dropping it
removes an optional feature?

Andreas