From 33917f35104f58e49f5fdd68756fad7382c35aae Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Jan 2020 17:35:26 +0100 Subject: [PATCH] Made argument for '--progress' optional --- src/storm/settings/modules/GeneralSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index 67244b163..aa4407d69 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/src/storm/settings/modules/GeneralSettings.cpp @@ -38,7 +38,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "'frequent' for frequently used options, 'all' for the complete help, or a regular expression to show help for all matching entities.").setDefaultValueString("frequent").makeOptional().build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, showProgressOptionName, false, "Sets when additional information (if available) about the progress is printed.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait (in seconds) between emitting information (0 means never print progress).").setDefaultValueUnsignedInteger(5).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, showProgressOptionName, false, "Sets when additional information (if available) about the progress is printed.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait (in seconds) between emitting information (0 means never print progress).").setDefaultValueUnsignedInteger(5).makeOptional().build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)