Browse Source

GUI bug fix: disable double-click for new sim path as appropriate.

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

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

@ -1879,7 +1879,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{
if(e.getClickCount() == 2 && e.getSource() == pathTablePlaceHolder)
{
a_newPath();
if (newPath.isEnabled()) a_newPath();
}
if(e.isPopupTrigger() && (e.getSource() == pathTablePlaceHolder || e.getSource() == pathTable || e.getSource() == pathTable.getTableHeader() || e.getSource() == tableScroll))
{

Loading…
Cancel
Save