chore(library/module_mgr): comment unreachable_code assertion

@gebner, could you please take a look a check whether there is a better fix.
This commit is contained in:
Leonardo de Moura 2017-01-15 23:18:44 +01:00
parent 67226269b4
commit eabbc5bb68

View file

@ -65,7 +65,14 @@ static module_loader mk_loader(module_id const & cur_mod, std::vector<module_inf
}
}
} catch (std::out_of_range) {
lean_unreachable();
/* The following line of code is reachable.
Repro: create a file containing an "open" comment block.
Example:
/-
def x := 10
*/
// lean_unreachable();
}
throw exception(sstream() << "could not resolve import: " << import.m_name);
};