From a2140141a3bba6d628c5bd61b0cbcf09aaebe813 Mon Sep 17 00:00:00 2001
From: hbruintjes <h.bruintjes@cs.rwth-aachen.de>
Date: Wed, 29 Jun 2016 18:05:56 +0200
Subject: [PATCH] Fix virtual destructor
Former-commit-id: ff3ee6cafac3985054bedc09593d6c645dd4c0b1
---
src/settings/modules/ModuleSettings.h | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/settings/modules/ModuleSettings.h b/src/settings/modules/ModuleSettings.h
index 08c92909d..2145d5267 100644
--- a/src/settings/modules/ModuleSettings.h
+++ b/src/settings/modules/ModuleSettings.h
@@ -30,6 +30,7 @@ namespace storm {
* @param moduleName The name of the module for which to build the settings.
*/
ModuleSettings(std::string const& moduleName);
+ virtual ~ModuleSettings() {}
/*!
* Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
@@ -140,4 +141,4 @@ namespace storm {
} // namespace settings
} // namespace storm
-#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */
\ No newline at end of file
+#endif /* STORM_SETTINGS_MODULES_MODULESETTINGS_H_ */