From effbf78d363b6c890874bc46f19f697cdc33bf5e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Dec 2014 16:13:29 -0800
Subject: [PATCH] fix(shell): use --server for .hlean files

---
 src/shell/lean.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index bdf23aedb..27c8675ad 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -515,7 +515,7 @@ int main(int argc, char ** argv) {
                 lean::display_error(diagnostic(env, ios), &pp, ex);
             }
         }
-        if (ok && server && default_k == input_kind::Lean) {
+        if (ok && server && (default_k == input_kind::Lean || default_k == input_kind::HLean)) {
             signal(SIGINT, on_ctrl_c);
             ios.set_option(lean::name("pp", "beta"), true);
             lean::server Sv(env, ios, num_threads);