/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2024-06-11 14:18 +0200 806 accelerator_font
-rw-r--r-- 2024-06-11 14:18 +0200 1732 docking
-rw-r--r-- 2024-06-11 14:18 +0200 4359 extended_styles_brackets
-rw-r--r-- 2024-06-11 14:18 +0200 1691 folding
-rw-r--r-- 2024-06-11 14:18 +0200 576 laf_fonts
-rw-r--r-- 2024-06-11 14:18 +0200 1232 panel_font
-rw-r--r-- 2024-06-11 14:18 +0200 892 props
-rw-r--r-- 2024-06-11 14:18 +0200 2334 putenv
-rw-r--r-- 2024-06-11 14:18 +0200 765 title
-rw-r--r-- 2024-06-11 14:18 +0200 787 vfs_manager
-rw-r--r-- 2024-06-11 14:18 +0200 2619 vfs_marker