GitLab

Note there's a typo here and using https doesn't seem to work.

This reverts commit df8b6026.

Tomaz Canabrava authored Jul 19, 2020 and Tomaz Canabrava committed Jul 19, 2020

This reduces buildtime when touching on unrelated Filter
classes.

Thomas Surrel authored Jul 16, 2020 and Kurt Hindenburg committed Jul 17, 2020

This patch improves the highlightScrolledLines feature in several ways:
- fixes some inconsistences in its behavior
- optimizes the region that needs to be repainted
- fixes cases where the highlight was not cleared correclty when
  changing some  profile properties (e.g. the scroll bar position)