diff options
Diffstat (limited to 'config/companion_libs/gmp.in')
| -rw-r--r-- | config/companion_libs/gmp.in | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/config/companion_libs/gmp.in b/config/companion_libs/gmp.in new file mode 100644 index 0000000..0ac2b2c --- /dev/null +++ b/config/companion_libs/gmp.in @@ -0,0 +1,32 @@ +# GMP options + +choice + bool + prompt "GMP version" + +config GMP_V_4_2_2 + bool + prompt "4.2.2" + +config GMP_V_4_2_4 + bool + prompt "4.2.4" + +# CT_INSERT_VERSION_ABOVE +# Don't remove above line! +endchoice + +config GMP_VERSION + string + default "4.2.2" if GMP_V_4_2_2 + default "4.2.4" if GMP_V_4_2_4 +# CT_INSERT_VERSION_STRING_ABOVE +# Don't remove above line! + +config GMP_CHECK + bool + prompt "Check GMP" + default y + help + It is highly recommended that 'make check' is run against the newly built + GMP library. See http://gmplib.org/ |