better rounding of font size

This commit is contained in:
hneemann 2017-05-10 13:18:25 +02:00
parent 92af0a7dc8
commit 8e4ac7348c

View File

@ -3,6 +3,7 @@ package de.neemann.gui;
/*
* Win 150% : getScreenResolution() = 144
* Win 100% : getScreenResolution() = 96
* Linux : getScreenResolution() = 95
*/
import javax.swing.*;
@ -37,7 +38,7 @@ public final class Screen {
float scaling = 1;
int size = 12;
try {
int s = Toolkit.getDefaultToolkit().getScreenResolution() * 12 / 96;
int s = Math.round(Toolkit.getDefaultToolkit().getScreenResolution() * 12 / 96f);
if (s > 12) {
scaling = s / 12f;
size = s;