From ce6e0d8c0d8882b627d1c2b1ffc647fe03fa484a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 25 Jan 2012 10:26:35 +0000 Subject: [PATCH] Disable start-up warning messages about unknown options in .prism file. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4478 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismSettings.java | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index b1d1af48..5ff41f86 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -609,15 +609,20 @@ public class PrismSettings implements Observer } else { - // Make sure this is not an old PRISM setting and if not print a warning - boolean isOld = false; - for (int i = 0; i < oldPropertyNames.length; i++) { - if (oldPropertyNames[i].equals(key)) { - isOld = true; - break; + // Warning for unused options disabled for now + // (it's a pain when you have lots of branches with lots of new options) + if (false) { + // Make sure this is not an old PRISM setting and if not print a warning + boolean isOld = false; + for (int i = 0; i < oldPropertyNames.length; i++) { + if (oldPropertyNames[i].equals(key)) { + isOld = true; + break; + } } + if (!isOld) + System.err.println("Warning: PRISM setting \"" + key + "\" is unknown."); } - if (!isOld) System.err.println("Warning: PRISM setting \""+key+"\" is unknown."); } } }