fix(shell/lean): Flycheck doesn't ignore stderr

2018-09-12 08:28:50 -07:00 · 2018-09-12 08:28:50 -07:00 · 62671c8b6f
commit 62671c8b6f
parent de2abf5d8c
1 changed files with 2 additions and 1 deletions
--- 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) {