diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-11-08 13:41:21 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-08 13:41:21 -0800 |
| commit | e50e990e5a0a85c5e36c6a6b6d8a59c3482b08fb (patch) | |
| tree | 3b981f3ca75cc788cd934f5d18215c14c51060ce /src/util | |
| parent | cbd86eb4ed8bafc17f28244b746a376a019462f1 (diff) | |
cmake: Disable C++ GNU extensions. (#3446)
Fixes #971.
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/statistics_registry.h | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index a369be272..4d4cc76df 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -780,11 +780,7 @@ public: /** * Resource-acquisition-is-initialization idiom for statistics * registry. Useful for stack-based statistics (like in the driver). - * Generally, for statistics kept in a member field of class, it's - * better to use the above KEEP_STATISTIC(), which does declaration of - * the member, construction of the statistic, and - * registration/unregistration. This RAII class only does - * registration and unregistration. + * This RAII class only does registration and unregistration. */ class CVC4_PUBLIC RegisterStatistic { public: |