Browse Source

cli: don't print the whole help message when an error occurred during option parsing.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
d6e91183d7
  1. 5
      src/storm-cli-utilities/cli.cpp

5
src/storm-cli-utilities/cli.cpp

@ -177,8 +177,7 @@ namespace storm {
try {
storm::settings::mutableManager().setFromCommandLine(argc, argv);
} catch (storm::exceptions::OptionParserException& e) {
storm::settings::manager().printHelp();
throw e;
STORM_LOG_ERROR("Unable to parse command line options. Type 'storm --help' or 'storm --help all' for help.");
return false;
}
@ -186,7 +185,7 @@ namespace storm {
bool result = true;
if (general.isHelpSet()) {
storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpModuleName());
storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpFilterExpression());
result = false;
}

Loading…
Cancel
Save