From 541e9010e12bfe70dd3a67cacdcb2c801ee50b65 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Oct 2016 12:56:50 -0700
Subject: [PATCH] fix(shell/lean): disable initialize/finalize server when
 -DSERVER=OFF is used

---
 src/shell/lean.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index ec1d754e59..3f7e87aed8 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -224,10 +224,14 @@ private:
     lean::initializer m_init;
 public:
     initializer() {
+#if defined(LEAN_SERVER)
         lean::initialize_server();
+#endif
     }
     ~initializer() {
+#if defined(LEAN_SERVER)
         lean::finalize_server();
+#endif
     }
 };