max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(shell/lean): do not repeat progress messages

Browse source 
This should fix the problem with the 4MB log limit on Travis.
This commit is contained in:
Gabriel Ebner 2017-06-29 13:04:27 +02:00
parent bfed11a6f7
commit ee94f7688c
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/shell/lean.cpp
View file

@ -232,6 +232,7 @@ class progress_message_stream {
bool m_show_progress;
std::unique_ptr<single_timer> m_timer;
std::string m_last_task;
void clear_shown_task() {
if (m_showing_task) {
@ -314,6 +315,8 @@ public:
void show_current_task_core() {
if (m_use_json) return;
if (auto desc = find_current_task()) {
if (*desc == m_last_task && m_showing_task) return;
m_last_task = *desc;
clear_shown_task();
#if defined(LEAN_EMSCRIPTEN)
m_out << *desc << std::endl;