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

feat(util/log_tree): inherit description

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-23 13:27:39 +01:00
parent c55579dd69
commit fdd80c12dd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/log_tree.cpp
View file

@ -125,7 +125,7 @@ log_tree::node log_tree::node::mk_child(name n, std::string const & description,
child.m_ptr->m_detached = m_ptr->m_detached;
}
child.m_ptr->m_detail_level = std::max(m_ptr->m_detail_level, lvl);
child.m_ptr->m_description = description;
child.m_ptr->m_description = description.empty() ? m_ptr->m_description : description;
child.m_ptr->m_location = loc;
m_ptr->m_children.insert(n, child);