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 /src/util/output.i | |
parent | 5d9fabc11757166679db9df874a0abe876aec0b8 (diff) |
fix swig-ignored interface name; hopefully fixes Debian package nightly builds
Diffstat (limited to 'src/util/output.i')
-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); |