From 4fa767be298c40ebb95b74d5016a0538c02212e6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 28 Mar 2012 18:22:32 +0000 Subject: [PATCH] fix swig-ignored interface name; hopefully fixes Debian package nightly builds --- src/util/output.i | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); -- 2.30.2