michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(shell): remove --permissive option, closes #107

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-29 13:26:07 -07:00
parent eeffb498b8
commit 5ebebb30a8
1 changed files with 3 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/shell/lean.cpp
View file

@ -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);
}