From 9bac91f5ef029885b190f048eecc46df7cd4dd4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Dec 2013 18:57:15 -0800
Subject: [PATCH] fix(frontends/lean): libreadline support

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt            | 2 +-
 src/frontends/lean/parser.cpp | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7cbdacfdfe..81df0f2e7d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -11,6 +11,7 @@ option(MULTI_THREAD       "MULTI_THREAD"       ON)
 option(BOOST              "BOOST"              OFF)
 option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
+option(READLINE           "READLINE"           OFF)
 
 # Added for CTest
 INCLUDE(CTest)
@@ -124,7 +125,6 @@ else()
 endif()
 
 # Readline
-option(READLINE "READLINE" OFF)
 if("${READLINE}" MATCHES "ON")
   find_package(Readline)
   set(EXTRA_LIBS ${EXTRA_LIBS} ${READLINE_LIBRARY})
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9901db52e8..97889cd827 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #ifdef LEAN_USE_READLINE
+#include <readline/readline.h>
+#include <readline/history.h>
 #include <stdlib.h>
 #include <stdio.h>
 #include <unistd.h>
 #include <algorithm>
-#include <readline/readline.h>
-#include <readline/history.h>
 #endif
 #include <utility>
 #include <string>