diff -r 5416f4ba36bf -r 5d9b7f52514f config/companion_libs/gmp.in
--- a/config/companion_libs/gmp.in	Sun May 03 21:10:15 2009 +0000
+++ b/config/companion_libs/gmp.in	Mon May 25 17:16:49 2009 +0000
@@ -25,8 +25,13 @@
 
 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.