michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(shell/lean): use locking also for the index file

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-12 21:50:08 -08:00
parent 4dc3764a02
commit edad31a9b1
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/shell/lean.cpp
View file

@ -544,6 +544,7 @@ int main(int argc, char ** argv) {
cache.save(out);
}
if (gen_index) {
exclusive_file_lock index_lock(index_name);
std::shared_ptr<lean::file_output_channel> out(new lean::file_output_channel(index_name.c_str()));
ios.set_regular_channel(out);
index.save(regular(env, ios));