--- 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",