Skip to content
GitLab
Explore
Sign in
improve handling of repainting for ranges
Code
Review changes
Check out branch
Download
Patches
Plain diff
Christoph Cullmann
requested to merge
work/improve_range_repaint
into
master
Jun 12, 2021
Overview
2
Commits
1
Pipelines
0
Changes
5
Expand
ensure we really repaint on attribute change
simplify the range updating using new line range API
Merge request reports