Browse Source

Tweaked some column headings in simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@517 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
commit
4d38da27da
  1. 6
      prism/src/userinterface/simulator/GUISimulator.java

6
prism/src/userinterface/simulator/GUISimulator.java

@ -2896,7 +2896,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (view.showSteps())
{
if (groupCount == groupIndex)
{ return "[ Step ]"; }
{ return "Step"; }
groupCount++;
}
@ -2904,7 +2904,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (view.canShowTime() && (view.showTime() || view.showCumulativeTime()))
{
if (groupCount == groupIndex)
{ return "[ Time ]"; }
{ return "Time"; }
groupCount++;
}
@ -2953,7 +2953,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (view.getVisibleRewardColumns().size() > 0)
{
if (groupCount == groupIndex)
{ return "[ Rewards ]"; }
{ return "Rewards"; }
groupCount++;
}

Loading…
Cancel
Save