mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

Remove unused warning_displayer.

Browse source
This commit is contained in:
Bruce Mitchener 2018-10-21 20:30:07 +07:00
parent a73cf590db
commit 7e35ce275a
1 changed files with 0 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/util/warning.h
View file

@ -33,26 +33,5 @@ void warning_msg(const char * msg, ...);
void format2ostream(std::ostream& out, char const* fmt, va_list args); void format2ostream(std::ostream& out, char const* fmt, va_list args);
class warning_displayer {
const char * m_msg;
bool m_displayed;
public:
warning_displayer(const char * msg):
m_msg(msg),
m_displayed(false) {
}
void sign() {
if (!m_displayed) {
warning_msg(m_msg);
m_displayed = true;
}
}
void reset() {
m_displayed = false;
}
};
#endif /* WARNING_H_ */ #endif /* WARNING_H_ */