From 37596d575ad853058e3f48acb42053512154e1dd Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 19 Jan 2016 14:35:07 +0100 Subject: [PATCH] Settings always initialized now Former-commit-id: 10764fa8b93681d3fee7aac57f2f56da4add314a --- src/settings/SettingsManager.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index fffb10366..01041f5cd 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -72,11 +72,12 @@ namespace storm { void SettingsManager::setFromString(std::string const& commandLineString) { if (commandLineString.empty()) { - return; + this->setFromExplodedString({}); + } else { + std::vector argumentVector; + boost::split(argumentVector, commandLineString, boost::is_any_of("\t ")); + this->setFromExplodedString(argumentVector); } - std::vector argumentVector; - boost::split(argumentVector, commandLineString, boost::is_any_of("\t ")); - this->setFromExplodedString(argumentVector); } void SettingsManager::setFromExplodedString(std::vector const& commandLineArguments) { @@ -548,4 +549,4 @@ namespace storm { return dynamic_cast(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName)); } } -} \ No newline at end of file +}