use the same font size on Windows and GNU/Linux

2018-09-26, Andrey Skvortsov