Browse Source

Changed meaning of version in settings info.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@915 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
commit
ff86cbd167
  1. 10
      prism/src/prism/PrismSettings.java

10
prism/src/prism/PrismSettings.java

@ -504,8 +504,9 @@ public class PrismSettings implements Observer
Setting set = settingFromHash(key);
if(set != null)
{
// If "version" of setting is newer than the version of the settings file, ignore
if (resaveNeeded && Prism.compareVersions(set.getVersion(), version) >= 0) continue;
// If the version of the settings file is not newer than the "version" of the setting,
// and we are re-saving the file, overwrite the setting with the default value
if (resaveNeeded && Prism.compareVersions(version, set.getVersion()) <= 0) continue;
try
{
Object valObj = set.parseStringValue(value);
@ -543,8 +544,9 @@ public class PrismSettings implements Observer
Setting set = settingFromHash(key);
if(set != null)
{
// If "version" of setting is newer than the version of the settings file, ignore
if (resaveNeeded && Prism.compareVersions(set.getVersion(), version) >= 0) continue;
// If the version of the settings file is not newer than the "version" of the setting,
// and we are re-saving the file, overwrite the setting with the default value
if (resaveNeeded && Prism.compareVersions(version, set.getVersion()) <= 0) continue;
try
{
Object valObj = set.parseStringValue(multiline.toString() + line);

Loading…
Cancel
Save