diff options
author | Norbert Preining <norbert@preining.info> | 2020-03-11 03:01:11 +0000 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2020-03-11 03:01:11 +0000 |
commit | 5412d52974c365e2d5bc1a8320816a729f7c10ab (patch) | |
tree | 5c8cee6076f9589a9d372c0ee08d16210251ac9a /support/makeglossariesgui/src/java/MakeGlossariesGUI.java | |
parent | 877268a0de707a979be934d888518f6cc02d73a6 (diff) |
CTAN sync 202003110301
Diffstat (limited to 'support/makeglossariesgui/src/java/MakeGlossariesGUI.java')
-rw-r--r-- | support/makeglossariesgui/src/java/MakeGlossariesGUI.java | 30 |
1 files changed, 28 insertions, 2 deletions
diff --git a/support/makeglossariesgui/src/java/MakeGlossariesGUI.java b/support/makeglossariesgui/src/java/MakeGlossariesGUI.java index 4fa64a1455..b809c8f329 100644 --- a/support/makeglossariesgui/src/java/MakeGlossariesGUI.java +++ b/support/makeglossariesgui/src/java/MakeGlossariesGUI.java @@ -1,3 +1,21 @@ +/* + Copyright (C) 2013-2020 Nicola L.C. Talbot + www.dickimaw-books.com + + This program is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA +*/ package com.dickimawbooks.makeglossariesgui; import java.io.*; @@ -121,6 +139,11 @@ public class MakeGlossariesGUI extends JFrame scrollPane = new JScrollPane(mainPanel); scrollPane.setPreferredSize(new Dimension(800,600)); + /* + * The font is only set for the main window not for the + * manual. HelpBroker.setFont(Font) is lost whenever a new + * HTML file is loaded. + */ setFont(new Font(invoker.getProperties().getFontName(), invoker.getProperties().getFontStyle(), invoker.getProperties().getFontSize())); @@ -656,8 +679,11 @@ public class MakeGlossariesGUI extends JFrame public void updateFont() { MakeGlossariesProperties properties = invoker.getProperties(); - setFont(new Font(properties.getFontName(), - properties.getFontStyle(), properties.getFontSize())); + + Font f = new Font(properties.getFontName(), + properties.getFontStyle(), properties.getFontSize()); + + setFont(f); updateAll(); } |