/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2025-01-08 15:00 +0100 1732 docking
-rw-r--r-- 2025-01-08 15:00 +0100 3999 extended_styles_brackets
-rw-r--r-- 2025-01-08 15:00 +0100 1691 folding
-rw-r--r-- 2025-01-08 15:00 +0100 839 laf_fonts
-rw-r--r-- 2025-01-08 15:00 +0100 2313 menus_and_sidekick
-rw-r--r-- 2025-01-08 15:00 +0100 1232 panel_font
-rw-r--r-- 2025-01-08 15:00 +0100 818 props
-rw-r--r-- 2025-01-08 15:00 +0100 4682 putenv
-rw-r--r-- 2025-01-08 15:00 +0100 660 title
-rw-r--r-- 2025-01-08 15:00 +0100 787 vfs_manager
-rw-r--r-- 2025-01-08 15:00 +0100 2619 vfs_marker