Milky/selection border#13

Open

milkmanmatty wants to merge 11 commits intoMHeasell:masterfrom

milkmanmatty:milky/selection-border

Commits on May 30, 2022

Commits on Jun 2, 2022

Force repaint on selection change to remove "burn-in" of previous selection border.
Matt
committed