From e6566e58149c1b655655c60970fedce3a04942be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 May 2015 18:13:44 -0700 Subject: [PATCH] fix(frontends/lean/parser): incorrect error message --- src/frontends/lean/parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 64838b96d..b1097fdfe 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -111,7 +111,7 @@ parser::parser(environment const & env, io_state const & ios, m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { m_profile = ios.get_options().get_bool("profile", false); - if (num_threads > 1) + if (num_threads > 1 && m_profile) throw exception("option --profile cannot be used when theorems are compiled in parallel"); m_has_params = false; m_keep_theorem_mode = tmode;