diff -r 655ee0516997 -r 5416f4ba36bf config/gmp_mpfr/gmp.in --- a/config/gmp_mpfr/gmp.in Sat May 02 22:21:53 2009 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -# 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/