diff options
Diffstat (limited to 'src/main/interactive_shell.cpp')
| -rw-r--r-- | src/main/interactive_shell.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 0ddd8707a..e6ae7ad5d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -261,7 +261,7 @@ restart: if (!d_usingEditline) { /* Extract the newline delimiter from the stream too */ - int c CVC4_UNUSED = d_in.get(); + int c CVC5_UNUSED = d_in.get(); Assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; |