diff options
Diffstat (limited to 'src/printer/printer.h')
| -rw-r--r-- | src/printer/printer.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h index 04b435060..8d1931a83 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -53,11 +53,11 @@ public: /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, - int toDepth, bool types) const throw() = 0; + int toDepth, bool types, size_t dag) const throw() = 0; /** Write a Command out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const throw() = 0; + int toDepth, bool types, size_t dag) const throw() = 0; /** Write a CommandStatus out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; |