--- a/src/Pure/GUI/gui.scala Sun Nov 29 21:58:40 2020 +0100
+++ b/src/Pure/GUI/gui.scala Sun Nov 29 23:23:32 2020 +0100
@@ -251,6 +251,7 @@
val default_font = label_font()
val ui = UIManager.getDefaults
for (prop <- List(
+ "ToggleButton.font",
"CheckBoxMenuItem.font",
"Label.font",
"Menu.font",