src/Pure/Admin/component_jedit.scala
changeset 82420 0fc508521b2a
parent 82415 eaf11864fb71
child 82421 b684876ab760
--- 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