# HG changeset patch
# User wenzelm
# Date 1743780665 -7200
# Node ID 21f7f29ef9cbc3d953ac8dd4c010b237f381dad6
# Parent  314d6b215f9008cd4cc3a1934cd91b880b1e1749
proper hyperlink column (amending 6898054035d6);

diff -r 314d6b215f90 -r 21f7f29ef9cb src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 16:35:05 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 17:31:05 2025 +0200
@@ -238,7 +238,7 @@
     if (snapshot.is_outdated) None
     else {
       snapshot.find_command_position(id, offset)
-        .map(pos => hyperlink_file(focus, pos.name, line = pos.line))
+        .map(pos => hyperlink_file(focus, pos.name, line = pos.line, offset = pos.column))
     }
   }