/src/Tools/jEdit/patches/
drwxr-xr-x [up]
-rw-r--r-- 2015-03-31 20:18 +0200 2388 brackets
-rw-r--r-- 2015-03-31 20:18 +0200 2400 content_margin
-rw-r--r-- 2015-03-31 20:18 +0200 1917 docking
-rw-r--r-- 2015-03-31 20:18 +0200 3719 extended_styles
-rw-r--r-- 2015-03-31 20:18 +0200 1691 folding
-rw-r--r-- 2015-03-31 20:18 +0200 1604 numeric_keypad
-rw-r--r-- 2015-03-31 20:18 +0200 2311 sorted_properties
-rw-r--r-- 2015-03-31 20:18 +0200 1386 structure_matcher