diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-05-28 21:46:54 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-28 19:46:54 +0000 |
| commit | 15d38800b9f493fcf4573160b420f0ab9563b4a8 (patch) | |
| tree | bf3fd421a1f5f6b2d7d0cad93d7b513a2d71e5a2 /src/options/module_template.cpp | |
| parent | f4894f5e0630bd3610699b13a8abae3e0ce9e600 (diff) | |
Add non-templated method to set option defaults (#6540)
This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.
Diffstat (limited to 'src/options/module_template.cpp')
| -rw-r--r-- | src/options/module_template.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index c79656e4b..bc953b952 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -33,6 +33,14 @@ ${defs}$ ${modes}$ + +namespace ${id}$ +{ +// clang-format off +${defaults}$ +// clang-format on +} + } // namespace options } // namespace cvc5 // clang-format on |