diff options
author | Tom Rondeau <tom@trondeau.com> | 2014-07-03 18:39:01 -0400 |
---|---|---|
committer | Tom Rondeau <tom@trondeau.com> | 2014-07-03 18:39:01 -0400 |
commit | 085c35a375468179929b690a0d7f037dc6ef23bf (patch) | |
tree | 6891061331c5fea7e962386d31c3235f7e2bc6cb /grc/gui/Preferences.py | |
parent | 4ca2456b0120a6d1468665a6afd2094ad2da8998 (diff) |
volk: adds command-line option to enable/disable use of ORC with -DENABLE_ORC=True/False.
If ORC is found on the system, the default is to use it. If we have ORC but don't want to use it, we can turn it off using this.
Diffstat (limited to 'grc/gui/Preferences.py')
0 files changed, 0 insertions, 0 deletions