/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2020-07-02 12:10 +0000 804 accelerator_font
-rw-r--r-- 2020-07-02 12:10 +0000 1730 docking
-rw-r--r-- 2020-07-02 12:10 +0000 2442 extended_styles
-rw-r--r-- 2020-07-02 12:10 +0000 1689 folding
-rw-r--r-- 2020-07-02 12:10 +0000 816 props
-rw-r--r-- 2020-07-02 12:10 +0000 2332 putenv
-rw-r--r-- 2020-07-02 12:10 +0000 763 title
-rw-r--r-- 2020-07-02 12:10 +0000 785 vfs_manager
-rw-r--r-- 2020-07-02 12:10 +0000 2613 vfs_marker