From 92aa058d85e64e670b693db99cc08c571ae4150b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 4 Oct 2007 12:54:39 +0000 Subject: [PATCH] Button label in simulator. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@440 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/simulator/GUISimulator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index fc81af25..08ed3e5b 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -1262,7 +1262,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect randomExplorationButton.setIcon(new javax.swing.ImageIcon("")); randomExplorationButton.setToolTipText("Make a number of random automatic updates"); randomExplorationButton.setHorizontalAlignment(javax.swing.SwingConstants.LEADING); - randomExplorationButton.setLabel("Random Exploration"); + randomExplorationButton.setLabel("Simulate"); randomExplorationButton.setMaximumSize(new java.awt.Dimension(220, 23)); randomExplorationButton.setMinimumSize(new java.awt.Dimension(50, 23)); randomExplorationButton.setPreferredSize(new java.awt.Dimension(160, 23));