rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-03-15 12:29:26 +01:00
Code Issues Releases Activity

Added Platform.getSystemDPI() API

Browse Source
This commit is contained in:
Cristian Maglie 2016-11-03 16:29:41 +02:00
parent af70053218
commit d63162b5a1
2 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
app/src/processing/app/Theme.java
View File

@ -122,7 +122,7 @@ public class Theme {
return scale; return scale;
} catch (NumberFormatException ignore) { } catch (NumberFormatException ignore) {
} }
return 100; return BaseNoGui.getPlatform().getSystemDPI() * 100 / 96;
} }
static public int scale(int size) { static public int scale(int size) {

5
arduino-core/src/processing/app/Platform.java
View File

@ -333,4 +333,9 @@ public class Platform {
public void fixSettingsLocation() throws Exception { public void fixSettingsLocation() throws Exception {
//noop //noop
} }
public int getSystemDPI() {
return 96;
}
} }