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