diff options
Diffstat (limited to 'config/companion_libs/gmp.in')
| -rw-r--r-- | config/companion_libs/gmp.in | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/config/companion_libs/gmp.in b/config/companion_libs/gmp.in index 0ac2b2c..3690c97 100644 --- a/config/companion_libs/gmp.in +++ b/config/companion_libs/gmp.in @@ -25,8 +25,13 @@ config GMP_VERSION config GMP_CHECK bool - prompt "Check GMP" - default y + prompt "Check GMP (!!! README !!!)" + default n help - It is highly recommended that 'make check' is run against the newly built - GMP library. See http://gmplib.org/ + It is highly recommended to check the newly built GMP library. + Unfortunately, this is a very intensive task, and takes a loooong time. + + Checking GMP is thus disabled by default. + + If you suspect that your GMP library is the cause for incorrectly + generated code, you should answer 'Y' here. |