diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-02 20:29:27 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-02 18:29:27 +0000 |
| commit | 5516d995582f5ccfa6e8dcc17d6b7e3f0c56551a (patch) | |
| tree | b1a6366ac1928e85dc0d499ab9cb1fe354e6917d /src/options/options_public_functions.cpp | |
| parent | 2506e17ca86c42b7590f65326b70a69b0efdb0bd (diff) | |
New statistics registry (#6210)
This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.
Diffstat (limited to 'src/options/options_public_functions.cpp')
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 1bccc283f..3ccf3b744 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -126,11 +126,11 @@ bool Options::getSemanticChecks() const{ bool Options::getStatistics() const{ // statsEveryQuery enables stats - return (*this)[options::statistics] || (*this)[options::statsEveryQuery]; + return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery]; } bool Options::getStatsEveryQuery() const{ - return (*this)[options::statsEveryQuery]; + return (*this)[options::statisticsEveryQuery]; } bool Options::getStatsHideZeros() const{ |