summaryrefslogtreecommitdiff
path: root/config/companion_libs/ppl.in
diff options
context:
space:
mode:
Diffstat (limited to 'config/companion_libs/ppl.in')
-rw-r--r--config/companion_libs/ppl.in14
1 files changed, 0 insertions, 14 deletions
diff --git a/config/companion_libs/ppl.in b/config/companion_libs/ppl.in
index d8f5906..efdeabf 100644
--- a/config/companion_libs/ppl.in
+++ b/config/companion_libs/ppl.in
@@ -17,17 +17,3 @@ config PPL_VERSION
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.