diff options
| author | Tim King <taking@google.com> | 2016-02-01 11:25:29 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-02-01 11:25:29 -0800 |
| commit | 52685068705546798b0a4d8204b10b848213975a (patch) | |
| tree | 0e3de3d9959c8c6c4c3b780b5028e3bfb379f2a9 /src/base | |
| parent | cbfd4e87765b716e8d21bd115f5917edef63f8a4 (diff) | |
Fixing a potentially malformed template expansion when Dump() is disabled.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/output.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/base/output.h b/src/base/output.h index 4bffad85f..9d1ab03ae 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -110,6 +110,8 @@ public: bool isConnected() { return d_os != NULL; } operator std::ostream&() { return isConnected() ? *d_os : null_os; } + std::ostream* getStreamPointer() { return d_os; } + template <class T> CVC4ostream& operator<<(T const& t) CVC4_PUBLIC; |