projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9547f16) | patch
Remove setDefaults methods (#7413)
authorGereon Kremer <nafur42@gmail.com>
Tue, 19 Oct 2021 19:33:25 +0000 (12:33 -0700)
committerGitHub <noreply@github.com>
Tue, 19 Oct 2021 19:33:25 +0000 (14:33 -0500)
commit71842aa75ca106b14ded148a73ac856f3ecf5912
tree5131e46e5a4dd34f90972499d299332f58444fe3tree
parent9547f16cd326b71a41e96a42d094170e426561a4commit | diff
Remove setDefaults methods (#7413)

This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.
src/options/mkoptions.py diff | blob | history
src/options/module_template.cpp diff | blob | history
src/options/module_template.h diff | blob | history
src/options/options_handler.cpp diff | blob | history