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

fix(module_mgr): produce olean files with correct mtimes

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-06 09:58:34 +01:00 • committed by Leonardo de Moura
parent 15eaf30192
commit 70e41305e5
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/library/module_mgr.cpp
View file

@ -306,7 +306,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
mod->m_deps);
if (m_save_olean)
get_global_task_queue()->submit<olean_compilation_task>(mod);
mod->m_olean_task = get_global_task_queue()->submit<olean_compilation_task>(mod);
get_global_task_queue()->cancel_if([=] (generic_task * t) {
return t->get_version() < m_current_period && t->get_module_id() == id && t->get_pos() >= task_pos;