From b88165f27cdca16892b3fd7c61f6b82eae6432e3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 10 Nov 2015 15:58:19 +0100 Subject: [PATCH] fixed the warnings related to our macros Former-commit-id: 526b6ea95666ad6d4a5bcaef68c1d68877f59da8 --- src/settings/OptionBuilder.h | 2 +- src/utility/macros.h | 20 ++++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index 622a7cb1c..f70ac7c2a 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -85,7 +85,7 @@ namespace storm { * @return The resulting option. */ std::shared_ptr