Browse Source

Settings always initialized now

Former-commit-id: 10764fa8b9
tempestpy_adaptions
Mavo 9 years ago
parent
commit
37596d575a
  1. 5
      src/settings/SettingsManager.cpp

5
src/settings/SettingsManager.cpp

@ -72,12 +72,13 @@ namespace storm {
void SettingsManager::setFromString(std::string const& commandLineString) { void SettingsManager::setFromString(std::string const& commandLineString) {
if (commandLineString.empty()) { if (commandLineString.empty()) {
return;
}
this->setFromExplodedString({});
} else {
std::vector<std::string> argumentVector; std::vector<std::string> argumentVector;
boost::split(argumentVector, commandLineString, boost::is_any_of("\t ")); boost::split(argumentVector, commandLineString, boost::is_any_of("\t "));
this->setFromExplodedString(argumentVector); this->setFromExplodedString(argumentVector);
} }
}
void SettingsManager::setFromExplodedString(std::vector<std::string> const& commandLineArguments) { void SettingsManager::setFromExplodedString(std::vector<std::string> const& commandLineArguments) {
// In order to assign the parsed arguments to an option, we need to keep track of the "active" option's name. // In order to assign the parsed arguments to an option, we need to keep track of the "active" option's name.

Loading…
Cancel
Save