/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2025-04-22 22:11 +0200 1732 docking
-rw-r--r-- 2025-04-22 22:11 +0200 2757 emacs_macros
-rw-r--r-- 2025-04-22 22:11 +0200 4166 extended_styles_brackets
-rw-r--r-- 2025-04-22 22:11 +0200 1691 folding
-rw-r--r-- 2025-04-22 22:11 +0200 624 gutter
-rw-r--r-- 2025-04-22 22:11 +0200 28480 icons
-rw-r--r-- 2025-04-22 22:11 +0200 839 laf_fonts
-rw-r--r-- 2025-04-22 22:11 +0200 1189 line_separator
-rw-r--r-- 2025-04-22 22:11 +0200 2243 menus_and_sidekick
-rw-r--r-- 2025-04-22 22:11 +0200 1232 panel_font
-rw-r--r-- 2025-04-22 22:11 +0200 1576 props
-rw-r--r-- 2025-04-22 22:11 +0200 4682 putenv
-rw-r--r-- 2025-04-22 22:11 +0200 625 search_bar
-rw-r--r-- 2025-04-22 22:11 +0200 660 title
-rw-r--r-- 2025-04-22 22:11 +0200 787 vfs_manager
-rw-r--r-- 2025-04-22 22:11 +0200 2619 vfs_marker