/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2025-05-18 14:33 +0000 1732 docking
-rw-r--r-- 2025-05-18 14:33 +0000 2757 emacs_macros
-rw-r--r-- 2025-05-18 14:33 +0000 3175 extended_styles_brackets
-rw-r--r-- 2025-05-18 14:33 +0000 1691 folding
-rw-r--r-- 2025-05-18 14:33 +0000 44978 gui
-rw-r--r-- 2025-05-18 14:33 +0000 624 gutter
-rw-r--r-- 2025-05-18 14:33 +0000 839 laf_fonts
-rw-r--r-- 2025-05-18 14:33 +0000 1189 line_separator
-rw-r--r-- 2025-05-18 14:33 +0000 5196 menu_accelerator
-rw-r--r-- 2025-05-18 14:33 +0000 1232 panel_font
-rw-r--r-- 2025-05-18 14:33 +0000 1576 props
-rw-r--r-- 2025-05-18 14:33 +0000 4682 putenv
-rw-r--r-- 2025-05-18 14:33 +0000 636 status_bar
-rw-r--r-- 2025-05-18 14:33 +0000 660 title
-rw-r--r-- 2025-05-18 14:33 +0000 787 vfs_manager
-rw-r--r-- 2025-05-18 14:33 +0000 2043 vfs_marker