# HG changeset patch # User wenzelm # Date 1743772991 -7200 # Node ID 64eeb82f8b02f7226324be73d68195d3345e98b2 # Parent 84d5590b40c19d2e722664d8f69e3059325ee0e7 tuned signature; diff -r 84d5590b40c1 -r 64eeb82f8b02 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 15:18:04 2025 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 15:23:11 2025 +0200 @@ -115,8 +115,8 @@ focus: Boolean, view: View, name: String, - offset: Text.Offset = -1, - line: Int = -1 + line: Int = -1, + offset: Text.Offset = -1 ): Unit = { GUI_Thread.require {}