From 6da53bf87e6a9bfdec26b7b07f092ff8cadf0e19 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 13 Oct 2016 16:09:14 -0400 Subject: [PATCH] fix(shell/emscripten): reenable flycheck output --- src/shell/emscripten.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/shell/emscripten.cpp b/src/shell/emscripten.cpp index 701d863a1c..ba35d04571 100644 --- a/src/shell/emscripten.cpp +++ b/src/shell/emscripten.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "library/flycheck.h" #include "library/module.h" #include "library/standard_kernel.h" #include "library/type_context.h" @@ -23,8 +24,9 @@ private: io_state ios; public: - emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1), opts("flycheck", true), + emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1), env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()) { + ios.set_message_channel(std::make_shared(std::cout)); } int import_module(std::string mname) {