From a47945a93184893d6c3f81acfa6b2a269f072294 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 31 Jul 2019 19:03:02 +0200 Subject: [PATCH] Cleaner output when exporting schedulers --- src/storm-cli-utilities/model-handling.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index fd88471c5..f4f133b8a 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -773,7 +773,7 @@ namespace storm { if (ioSettings.isExportSchedulerSet()) { if (result->template asExplicitQuantitativeCheckResult().hasScheduler()) { auto const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); - STORM_PRINT_AND_LOG("Exporting scheduler to '" << ioSettings.getExportSchedulerFilename()) + STORM_PRINT_AND_LOG("Exporting scheduler ... ") storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename()); } else { STORM_LOG_ERROR("Scheduler requested but could not be generated.");