From 62671c8b6f01aa14bccfaa00f1fd41286e41a54b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 12 Sep 2018 08:28:50 -0700 Subject: [PATCH] fix(shell/lean): Flycheck doesn't ignore stderr --- src/shell/lean.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 105be54fbb..bacddaa529 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -523,7 +523,8 @@ int main(int argc, char ** argv) { } } - display_cumulative_profiling_times(std::cerr); + if (!json_output) + display_cumulative_profiling_times(std::cerr); if (!test_suite) { for (auto & mod : mods) {