tree 3fe69b1b33717602cbbb7f85a8dc9328a1ca92eb
parent 285e1cd350eb852ea124518709054e0113ee08da
author Dani Megert <dmegert> 1503584348 +0200
committer Dani Megert <dmegert> 1503584348 +0200

Fixed bug 521373: MarginPainter no longer needs to be initialized after font change