diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 62afa20d9a..0541495e9a 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -962,6 +962,7 @@ static void emit_main_fn(std::ostream & out, environment const & env, module_nam else out << "lean::initialize_runtime_module();\n"; out << "initialize_" << mangle(m, false) << "();\n"; + out << "lean::scoped_task_manager tmanager(lean::hardware_concurrency());\n"; if (arity == 2) { out << "obj* in = lean::box(0);\n"; out << "int i = argc;\n";