diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 22:10:21 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 22:10:21 +0000 |
| commit | 842fd54de1da122f4c7274796550c2fe21c11db2 (patch) | |
| tree | fec6236bc8c3e3b92cd3759ed13f4acc7bc6c6d2 /src/util/command.h | |
| parent | e0fc2cbe091097d95dbe6dd2eb9b6416b75be279 (diff) | |
ELSEIF support and parser debugging with '-d parser'
Diffstat (limited to 'src/util/command.h')
| -rw-r--r-- | src/util/command.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/util/command.h b/src/util/command.h index b41be4592..57edfea01 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -30,6 +30,7 @@ namespace CVC4 { namespace CVC4 { std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; class CVC4_PUBLIC Command { public: |