From d6e91183d74f698a5d0e3a3899a6b22f966f000d Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 May 2019 18:50:56 +0200 Subject: [PATCH] cli: don't print the whole help message when an error occurred during option parsing. --- src/storm-cli-utilities/cli.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index e4a929445..90b198fa9 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/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().getHelpModuleName()); + storm::settings::manager().printHelp(storm::settings::getModule().getHelpFilterExpression()); result = false; }