diff -r c98e22c67e21 -r f67ad2dbf6d5 src/Pure/Admin/component_jedit.scala --- a/src/Pure/Admin/component_jedit.scala Thu Apr 17 00:07:15 2025 +0200 +++ b/src/Pure/Admin/component_jedit.scala Thu Apr 17 00:25:58 2025 +0200 @@ -376,10 +376,8 @@ 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=