Browse Source

Bugfix: GUI option 'clear properties on model load' now respected.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@49 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 20 years ago
parent
commit
7d7d06ef99
  1. 2
      prism/src/userinterface/properties/GUIMultiProperties.java

2
prism/src/userinterface/properties/GUIMultiProperties.java

@ -1149,7 +1149,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
}
else if(me.getID() == GUIModelEvent.NEW_LOAD_NOT_RELOAD_MODEL)
{
if(isNewAfterReceiveNewOrLoadModelNotification())
if (getPrism().getSettings().getBoolean(PrismSettings.PROPERTIES_CLEAR_LIST_ON_LOAD))
{
a_newList();
}

Loading…
Cancel
Save