projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
536c95e
)
add a guard for history saving, to enable building without GNU history library
author
Morgan Deters
<mdeters@gmail.com>
Tue, 4 Oct 2011 15:48:03 +0000
(15:48 +0000)
committer
Morgan Deters
<mdeters@gmail.com>
Tue, 4 Oct 2011 15:48:03 +0000
(15:48 +0000)
src/main/interactive_shell.cpp
patch
|
blob
|
history
diff --git
a/src/main/interactive_shell.cpp
b/src/main/interactive_shell.cpp
index 1d1f447be6496d03fe6588a1f24b979403954c37..ef576839c9c8b5960aaa7058a275d11942cbb39f 100644
(file)
--- a/
src/main/interactive_shell.cpp
+++ b/
src/main/interactive_shell.cpp
@@
-134,6
+134,7
@@
InteractiveShell::InteractiveShell(ExprManager& exprManager,
}/* InteractiveShell::InteractiveShell() */
InteractiveShell::~InteractiveShell() {
+#if HAVE_LIBREADLINE
int err = ::write_history(d_historyFilename.c_str());
if(err == 0) {
Notice() << "Wrote " << ::history_length << " lines of history to "
@@
-142,6
+143,7
@@
InteractiveShell::~InteractiveShell() {
Notice() << "Could not write history to " << d_historyFilename
<< ": " << strerror(err) << std::endl;
}
+#endif /* HAVE_LIBREADLINE */
}
Command* InteractiveShell::readCommand() {