diff options
Diffstat (limited to 'src/util/statistics.i')
| -rw-r--r-- | src/util/statistics.i | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/util/statistics.i b/src/util/statistics.i index 7cc737d6c..a14fc29dd 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -2,5 +2,7 @@ #include "util/statistics.h" %} -%include "util/statistics.h" +%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); +%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); +%include "util/statistics.h" |