Browse Source

Default value of new properties file label in GUI is now "true" so adding a new label is less problematic.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@162 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
commit
013b62f232
  1. 2
      prism/src/userinterface/properties/GUIPropLabelList.java

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

@ -176,7 +176,7 @@ public class GUIPropLabelList extends JTable
public void addLabel()
{
labels.add(new GUILabel("L"+labCount, null));
labels.add(new GUILabel("L"+labCount, new ExpressionTrue()));
parent.setModified(true);
fireTableRowsInserted(labels.size()-1, labels.size()-1);
labCount++;

Loading…
Cancel
Save