changeset 51534 | 123bd97fcea1 |
parent 50900 | 6d80709ab862 |
child 51535 | f2f480bc4223 |
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 11:26:13 2013 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 26 12:40:51 2013 +0100 @@ -30,7 +30,7 @@ reactions += { case MouseClicked(_, point, _, clicks, _) if clicks == 2 => val index = peer.locationToIndex(point) - if (index >= 0) jEdit.openFile(view, listData(index).node) + if (index >= 0) Hyperlink(listData(index).node).follow(view) } } status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)