From 61c042fa9cc90e7199208b22744d823168e50d14 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 23:14:33 +0000 Subject: [PATCH] Bug fix: axis fonts when loading/saving graphs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4690 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/graph/AxisSettings.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/userinterface/graph/AxisSettings.java b/prism/src/userinterface/graph/AxisSettings.java index 9f669aac..64c61b21 100644 --- a/prism/src/userinterface/graph/AxisSettings.java +++ b/prism/src/userinterface/graph/AxisSettings.java @@ -934,7 +934,7 @@ public class AxisSettings extends Observable implements SettingOwner Font numberFont = getNumberFont().f; axis.setAttribute("numberFontName", numberFont.getName()); - axis.setAttribute("numberFontSize", "" + headingFont.getSize()); + axis.setAttribute("numberFontSize", "" + numberFont.getSize()); axis.setAttribute("numberFontStyle", "" + numberFont.getStyle()); Color numberFontColor = getHeadingFont().c; @@ -994,7 +994,7 @@ public class AxisSettings extends Observable implements SettingOwner Color numberFontColor = Graph.parseColor(numberFontColourR, numberFontColourG, numberFontColourB); - setHeadingFont(new FontColorPair(numberFont, numberFontColor)); + setNumberFont(new FontColorPair(numberFont, numberFontColor)); // axis autoScale property boolean autoScale = Graph.parseBoolean(axis.getAttribute("autoscale"));