From 4d38da27da2c70f144583712928e183c01f7c805 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 8 Nov 2007 09:53:13 +0000 Subject: [PATCH] Tweaked some column headings in simulator. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@517 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/simulator/GUISimulator.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index eadd588d..552ccd09 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/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++; }