Separate the two uses of the configured value GMP_NUMB_BITS.
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.
Showing with 17 additions and 8 deletions