Commit 1901ff80 authored by Dr. Michael Petter's avatar Dr. Michael Petter

automatically scale font size to resolution

parent eeea509f
......@@ -41,6 +41,8 @@ public class Experimental {
}
}
public static void main(String[] args) throws BackingStoreException, IllegalArgumentException, IllegalAccessException{
int size = (int)(Toolkit.getDefaultToolkit().getScreenResolution()*.25);
System.setProperty("swing.plaf.metal.controlFont","DejaVu Sans Mono Book-"+size);
for (String s : experimentalRoot.childrenNames())
System.out.println(s);
......
......@@ -1516,7 +1516,10 @@ public class TTT extends JFrame {
public static void main(String[] args) throws NumberFormatException,
IOException {
if (!System.getProperty("os.name").startsWith("Windows")) {
int size = (int)(Toolkit.getDefaultToolkit().getScreenResolution()*.2);
System.setProperty("swing.plaf.metal.controlFont","DejaVu Sans Mono Book-"+size);
}
// parse command line options
for (int i = 0; i < args.length; ++i) {
if (args[i].length() == 2 && args[i].charAt(0) == '-') {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment