diff -r 000000000000 -r 48c12c696778 config/companion_libs/ppl.in
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/config/companion_libs/ppl.in	Tue May 05 22:04:20 2009 +0000
@@ -0,0 +1,33 @@
+# PPL options
+
+choice
+    bool
+    prompt "PPL version"
+
+config PPL_V_0_10_2
+    bool
+    prompt "0.10.2"
+
+# CT_INSERT_VERSION_ABOVE
+# Don't remove above line!
+endchoice
+
+config PPL_VERSION
+    string
+    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.