Fix for mac readline.
authorMorgan Deters <mdeters@cs.nyu.edu>
Wed, 18 Jun 2014 19:30:32 +0000 (15:30 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Wed, 18 Jun 2014 19:41:34 +0000 (15:41 -0400)
configure.ac
src/main/interactive_shell.cpp

index 629e1625b13bd461f1b12ed88dc7b10617d4e58b..31dec369b67d27cfd6e6defe44a2c7dadee69ed5 100644 (file)
@@ -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
index a19e23725142969976838c49417f69af829b29f2..7d3742cf47d9dc7f3320fb687558e5876f63c57f 100644 (file)
@@ -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);