diff options
Diffstat (limited to 'config/companion_libs/cloog.in')
| -rw-r--r-- | config/companion_libs/cloog.in | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/config/companion_libs/cloog.in b/config/companion_libs/cloog.in new file mode 100644 index 0000000..99779c9 --- /dev/null +++ b/config/companion_libs/cloog.in @@ -0,0 +1,19 @@ +# 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! |