diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/companion_libs.in | 1 | ||||
| -rw-r--r-- | config/companion_libs/cloog.in | 32 |
2 files changed, 33 insertions, 0 deletions
diff --git a/config/companion_libs.in b/config/companion_libs.in index d581d80..c95418b 100644 --- a/config/companion_libs.in +++ b/config/companion_libs.in @@ -49,6 +49,7 @@ config PPL_CLOOG if PPL_CLOOG source config/companion_libs/ppl.in +source config/companion_libs/cloog.in endif endmenu diff --git a/config/companion_libs/cloog.in b/config/companion_libs/cloog.in new file mode 100644 index 0000000..e67e79f --- /dev/null +++ b/config/companion_libs/cloog.in @@ -0,0 +1,32 @@ +# CLooG options + +choice + bool + prompt "CLooG/ppl version" + +config CLOOG_V_0_15_3 + bool + prompt "0.15.3" + +# CT_INSERT_VERSION_ABOVE +# Don't remove above line! +endchoice + +config CLOOG_VERSION + string + default "0.15.3" if CLOOG_V_0_15_3 +# CT_INSERT_VERSION_STRING_ABOVE +# Don't remove above line! + +config CLOOG_CHECK + bool + prompt "Check CLooG (!!! README !!!)" + default n + help + It is highly recommended to check the newly built CLooG library. + Unfortunately, this is a very intensive task, and takes a loooong time. + + Checking CLooG is thus disabled by default. + + If you suspect that your CLooG library is the cause for incorrectly + generated code, you should answer 'Y' here. |