diff options
Diffstat (limited to 'src/printer/printer.cpp')
| -rw-r--r-- | src/printer/printer.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 4e464f829..2d5ae58cd 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -388,7 +388,7 @@ void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out, void Printer::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { printUnknownCommand(out, "set-info"); } @@ -401,7 +401,7 @@ void Printer::toStreamCmdGetInfo(std::ostream& out, void Printer::toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { printUnknownCommand(out, "set-option"); } |