From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 18 Jun 2014 19:30:32 +0000 (-0400)
Subject: Fix for mac readline.
X-Git-Tag: cvc5-1.0.0~6768
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbdf393fa0ba314493260991ddc1a163e9d2bade;p=cvc5.git

Fix for mac readline.
---

diff --git a/configure.ac b/configure.ac
index 629e1625b..31dec369b 100644
--- a/configure.ac
+++ b/configure.ac
@@ -982,7 +982,7 @@ AC_LIB_ANTLR
 CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
 
 # Checks for header files and their contents.
-AC_CHECK_HEADERS([getopt.h unistd.h])
+AC_CHECK_HEADERS([getopt.h unistd.h ext/stdio_filebuf.h])
 
 # Checks for typedefs, structures, and compiler characteristics.
 #AC_HEADER_STDBOOL
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index a19e23725..7d3742cf4 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -43,7 +43,9 @@
 #if HAVE_LIBREADLINE
 #  include <readline/readline.h>
 #  include <readline/history.h>
-#  include <ext/stdio_filebuf.h>
+#  if HAVE_EXT_STDIO_FILEBUF_H
+#    include <ext/stdio_filebuf.h>
+#  endif /* HAVE_EXT_STDIO_FILEBUF_H */
 #endif /* HAVE_LIBREADLINE */
 
 using namespace std;
@@ -57,7 +59,9 @@ const string InteractiveShell::INPUT_FILENAME = "<shell>";
 
 #if HAVE_LIBREADLINE
 
+#if HAVE_EXT_STDIO_FILEBUF_H
 using __gnu_cxx::stdio_filebuf;
+#endif /* HAVE_EXT_STDIO_FILEBUF_H */
 
 char** commandCompletion(const char* text, int start, int end);
 char* commandGenerator(const char* text, int state);