src/Tools/jEdit/patches/gutter
changeset 64254 b1aef25ce8df
parent 61746 3df1b6a5837c