From 5ebebb30a816d25ffe1a5933454caa25558adb77 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Aug 2014 13:26:07 -0700 Subject: [PATCH] feat(shell): remove --permissive option, closes #107 Signed-off-by: Leonardo de Moura --- src/shell/lean.cpp | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 2baa52cab..f901214e7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -84,7 +84,6 @@ static void display_help(std::ostream & out) { std::cout << " --flycheck print structured error message for flycheck\n"; std::cout << " --cache=file -c load/save cached definitions from/to the given file\n"; std::cout << " --index=file -i store index for declared symbols in the given file\n"; - std::cout << " --permissive -P save .olean files even when errors were found\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -120,7 +119,6 @@ static struct option g_long_options[] = { {"cache", required_argument, 0, 'c'}, {"deps", no_argument, 0, 'D'}, {"flycheck", no_argument, 0, 'F'}, - {"permissive", no_argument, 0, 'P'}, {"index", no_argument, 0, 'i'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, @@ -129,9 +127,9 @@ static struct option g_long_options[] = { }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "PFDSqlupgvhj:012k:012s:012t:012o:c:i:"; +static char const * g_opt_str = "FDSqlupgvhj:012k:012s:012t:012o:c:i:"; #else -static char const * g_opt_str = "PFDSqlupgvhj:012k:012t:012o:c:i:"; +static char const * g_opt_str = "FDSqlupgvhj:012k:012t:012o:c:i:"; #endif class simple_pos_info_provider : public pos_info_provider { @@ -153,7 +151,6 @@ int main(int argc, char ** argv) { bool server = false; bool only_deps = false; bool flycheck = false; - bool permissive = false; unsigned num_threads = 1; bool use_cache = false; bool gen_index = false; @@ -172,9 +169,6 @@ int main(int argc, char ** argv) { case 'S': server = true; break; - case 'P': - permissive = true; - break; case 'v': display_header(std::cout); return 0; @@ -297,7 +291,7 @@ int main(int argc, char ** argv) { ios.set_regular_channel(out); index.save(regular(env, ios)); } - if (export_objects && (permissive || ok)) { + if (export_objects && ok) { std::ofstream out(output, std::ofstream::binary); export_module(out, env); }