1 files changed, 33 insertions, 0 deletions
diff --git a/config/companion_libs/ppl.in b/config/companion_libs/ppl.in
new file mode 100644
index 0000000..d8f5906
--- /dev/null
+++ b/config/companion_libs/ppl.in
@@ -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.