diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-03-28 18:22:32 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-03-28 18:22:32 +0000 |
| commit | 4fa767be298c40ebb95b74d5016a0538c02212e6 (patch) | |
| tree | 0e90539a5af16dc06a1e44e173e69bf9908653ab | |
| parent | 5d9fabc11757166679db9df874a0abe876aec0b8 (diff) | |
fix swig-ignored interface name; hopefully fixes Debian package nightly builds
| -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); |