src/Tools/jEdit/patches/gui
changeset 82654 60bd591ef3fc
parent 82636 692feb5e45e6