Browse Source

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
master
Dave Parker 14 years ago
parent
commit
ce6e0d8c0d
  1. 7
      prism/src/prism/PrismSettings.java

7
prism/src/prism/PrismSettings.java

@ -609,6 +609,9 @@ public class PrismSettings implements Observer
} }
else else
{ {
// 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 // Make sure this is not an old PRISM setting and if not print a warning
boolean isOld = false; boolean isOld = false;
for (int i = 0; i < oldPropertyNames.length; i++) { for (int i = 0; i < oldPropertyNames.length; i++) {
@ -617,7 +620,9 @@ public class PrismSettings implements Observer
break; break;
} }
} }
if (!isOld) System.err.println("Warning: PRISM setting \""+key+"\" is unknown.");
if (!isOld)
System.err.println("Warning: PRISM setting \"" + key + "\" is unknown.");
}
} }
} }
} }

Loading…
Cancel
Save