diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:58:57 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-05 23:58:57 +0000 |
| commit | db264e836f2878a3cf09a54f1c577ce516fb1bc5 (patch) | |
| tree | cb66211ad7f92b342bf8972f2a136d99b5b2fc81 /src/expr/node.h | |
| parent | a8d7333d8fb03c95ef3d1d7d9501076b97add756 (diff) | |
Reverting a fix from earlier today that fixed a Mac OS warning but completely broke Linux. :-(
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 9d852f195..0f4b55d4a 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -52,11 +52,6 @@ class NodeManager; template <bool ref_count> class NodeTemplate; -// For some reason these are instantiated with different visibility in different modules?? -// Fix by making their instantiations explicit, here. -template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<false> const& t) CVC4_PUBLIC; -template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<true> const& t) CVC4_PUBLIC; - /** * Exception thrown during the type-checking phase, it can be * thrown by node.getType(). |