src/Tools/jEdit/src/theories_dockable.scala
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)