src/Pure/Admin/component_jedit.scala
changeset 82552 f67ad2dbf6d5
parent 82550 6d5a169c3a22
child 82559 ddcf31575146
--- 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=