diff options
| -rw-r--r-- | src/util/output.i | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/output.i b/src/util/output.i index b9c0e32ee..e9f674240 100644 --- a/src/util/output.i +++ b/src/util/output.i @@ -9,7 +9,7 @@ // it tries to generate the getters and setters. For now, just ignore them. %ignore CVC4::null_sb; %ignore CVC4::null_os; -%ignore CVC4::DumpC::dump_cout; +%ignore CVC4::DumpOutC::dump_cout; %ignore operator<<; %ignore on(std::string); |