src/Tools/jEdit/patches/gutter
changeset 82894 a8e47bd31965
parent 82565 1033ed5d3972