diff options
| author |   Yann E. MORIN <devnull@localhost> | 2009-06-17 09:38:04 (GMT) |
|---|---|---|
| committer | Yann E. MORIN <devnull@localhost> | 2009-06-17 09:38:04 (GMT) |
| commit | 302dd084c2e782ea5fdbde1db9f1b2bcda5ac83f (patch) | |
| tree | 2bd1601131ca41844086fcdcaccffcc7438a66ee /config/companion_libs/ppl.in | |
| parent | a393a72f5f7b0f0f48f11782d70b255c6ca5f740 (diff) | |
| parent | a7ff05b022a8db08185486fa0fbf324f2ecd9d3e (diff) | |
[gcc] Merge the gcc-4.4 suport to the default branch, from 1407:83083566fdd0
Diffstat (limited to 'config/companion_libs/ppl.in')
| -rw-r--r-- | config/companion_libs/ppl.in | 14 |
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. |