From 8ef899ef1c58c54ea8a82ff038bde17ba854d8ed Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Mon, 4 Jul 2016 17:30:10 +0200 Subject: [PATCH] Fix log file name argument Former-commit-id: c13b4ca3ad7687e24710fe3ce2e16d4304159298 --- src/settings/modules/DebugSettings.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/settings/modules/DebugSettings.cpp b/src/settings/modules/DebugSettings.cpp index 0f37e7ce7..92e8de9a9 100644 --- a/src/settings/modules/DebugSettings.cpp +++ b/src/settings/modules/DebugSettings.cpp @@ -38,7 +38,7 @@ namespace storm { } std::string DebugSettings::getLogfilename() const { - return this->getOption(traceOptionName).getArgumentByName("filename").getValueAsString(); + return this->getOption(logfileOptionName).getArgumentByName("filename").getValueAsString(); } bool DebugSettings::isTestSet() const { @@ -47,4 +47,4 @@ namespace storm { } // namespace modules } // namespace settings -} // namespace storm \ No newline at end of file +} // namespace storm