diff -r 48c12c696778 -r 7f5563e3ec2d config/companion_libs/ppl.in
--- a/config/companion_libs/ppl.in	Tue May 05 22:04:20 2009 +0000
+++ b/config/companion_libs/ppl.in	Fri Jun 26 19:09:22 2009 +0200
@@ -17,17 +17,3 @@
     default "0.10.2" if PPL_V_0_10_2
 # CT_INSERT_VERSION_STRING_ABOVE
 # Don't remove above line!
-
-config PPL_CHECK
-    bool
-    prompt "Check PPL (!!! README !!!)"
-    default n
-    help
-      Checking PPL is very intensive and takes a loooong time.
-      The PPL folks do not recommend checking the library, but they do
-      not recommend not checking it, either.
-      
-      Checking PPL is thus disabled by default.
-      
-      If you suspect that your PPL library is the cause for incorrectly
-      generated code, you should answer 'Y' here.