diff -r 8d6af6ab7d4d -r 21ff9c1a4644 src/Pure/GUI/gui.scala --- 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",