From 62ab7177725e208933e583076c69ce43380af720 Mon Sep 17 00:00:00 2001
From: Matt Pass <matt@mattpass.com>
Date: Sat, 20 Apr 2013 16:06:29 +0100
Subject: [PATCH] Font size set from user settings

Updateable using settings screen, value in config.php
---
 editor.php | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/editor.php b/editor.php
index 182f25b..ea60662 100644
--- a/editor.php
+++ b/editor.php
@@ -24,7 +24,8 @@ if ($ICEcoder["theme"]=="default") {echo 'lib/editor.css';} else {echo $ICEcoder
 $activeLineBG = array_search($ICEcoder["theme"],array("eclipse","elegant","neat")) !== false ? "#ccc" : "#000";
 ?>">
 <style type="text/css">
-.CodeMirror {position: absolute; top: 0px; width: 100%; font-size: 13px; z-index: 1}
+/* Make sure this next one remains the 1st item, updated with JS */
+.CodeMirror {position: absolute; top: 0px; width: 100%; font-size: <?php echo $ICEcoder["fontSize"];?>; z-index: 1}
 .CodeMirror-scroll {} /* was: height: auto; overflow: visible */
 /* Make sure this next one remains the 3rd item, updated with JS */
 .cm-s-activeLine {background: <?php echo $activeLineBG;?> !important}