From 4e765e64caabe2f964a4cf57e3af90cb69662c59 Mon Sep 17 00:00:00 2001
From: Matt Pass <matt@mattpass.com>
Date: Sat, 20 Apr 2013 16:16:39 +0100
Subject: [PATCH] Establish font size

According to config setting
---
 index.php | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/index.php b/index.php
index 998ffb9..5ba0ad3 100644
--- a/index.php
+++ b/index.php
@@ -58,6 +58,9 @@ if (file_exists(dirname(__FILE__)."/plugins/jshint/jshint.js")) {
 	echo "];top.ICEcoder.theme = '";
 	echo $ICEcoder["theme"]=="default" ? 'icecoder' : $ICEcoder["theme"];
 	echo "'";
+	echo ";top.ICEcoder.fontSize = '";
+	echo $ICEcoder["fontSize"];
+	echo "'";
 	echo ';top.ICEcoder.openLastFiles = ';
 	echo $ICEcoder["openLastFiles"] ? 'true' : 'false';
 	echo ';top.ICEcoder.lineWrapping = ';