src/Tools/jEdit/patches/gutter
changeset 65328 2510b0ce28da
parent 61746 3df1b6a5837c
equal deleted inserted replaced
65327:e886aed88b2c 65328:2510b0ce28da