author | wenzelm |
Fri, 04 Apr 2025 15:23:11 +0200 | |
changeset 82431 | 64eeb82f8b02 |
parent 82430 | 84d5590b40c1 |
child 82432 | 314d6b215f90 |
--- 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 {}