diff -r 955c5d6c1acf -r 0fc508521b2a src/Pure/Admin/component_jedit.scala --- a/src/Pure/Admin/component_jedit.scala Wed Apr 02 23:22:59 2025 +0200 +++ b/src/Pure/Admin/component_jedit.scala Thu Apr 03 12:04:13 2025 +0200 @@ -342,8 +342,11 @@ metal.secondary.fontsize=12 navigate-backwards.label=Navigate backwards navigate-backwards.shortcut=AS+LEFT +navigate-backwards.icon=ArrowL.png navigate-forwards.label=Navigate forwards navigate-forwards.shortcut=AS+RIGHT +navigate-forwards.icon=ArrowR.png +navigate-toolbar=navigate-backwards navigate-forwards navigator.showOnToolbar=true new-file-in-mode.shortcut= next-bracket.shortcut2=C+e C+9