DrJava needs a way to change the default font size without recompiling the whole program. This will eventually be part of the larger configuration project, but it was deemed necessary enough to implement in the current config framework.
Logged In: YES user_id=429731
Implemented in drjava-20020611-1853.
Specify any of the following config options in your ".drjava" file:
# Definitions, interactions fonts font.main.name = Monospaced font.main.size = 12 font.main.style = 0
# Document selector font font.doclist.name = Monospaced font.doclist.size = 10 font.doclist.style = 0
The Style parameters take in the int value of the java.awt.Font constants. Plain is 0, Bold is 1, Italic is 2, and Bold Italic is 3.
Logged In: YES
user_id=429731
Implemented in drjava-20020611-1853.
Specify any of the following config options in your
".drjava" file:
# Definitions, interactions fonts
font.main.name = Monospaced
font.main.size = 12
font.main.style = 0
# Document selector font
font.doclist.name = Monospaced
font.doclist.size = 10
font.doclist.style = 0
The Style parameters take in the int value of the
java.awt.Font constants. Plain is 0, Bold is 1, Italic is
2, and Bold Italic is 3.