-
Niels Möller authored
In version.h, GMP_NUMB_BITS is needed only for mini-gmp builds. In non-mini-gmp builds, substitute a dummy value there, to make the contents of this header file platform independent. In Makefile, we always need a properly configured value, and do this with the renamed variable NUMB_BITS.
b7052093