diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 2a2de2ba0..b81d7269a 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -502,7 +502,7 @@ void parser_imp::parse_set_option() { name lean_id = name("lean") + id; decl_it = get_option_declarations().find(lean_id); if (decl_it == get_option_declarations().end()) { - throw parser_error(sstream() << "unknown option '" << id << "', type 'Help Options.' for list of available options", id_pos); + throw parser_error(sstream() << "unknown option '" << id << "', type 'help options.' for list of available options", id_pos); } else { id = lean_id; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 65a97b0be..9be435508 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -185,9 +185,9 @@ int main(int argc, char ** argv) { signal(SIGINT, on_ctrl_c); if (default_k == input_kind::Lean) { #if defined(LEAN_WINDOWS) - std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl; + std::cout << "Type 'exit.' to exit or 'help.' for help."<< std::endl; #else - std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; + std::cout << "Type Ctrl-D or 'exit.' to exit or 'help.' for help."<< std::endl; #endif shell sh(env, &S); int status = sh() ? 0 : 1;