Font size set from user settings

Updateable using settings screen, value in config.php
This commit is contained in:
Matt Pass
2013-04-20 16:06:29 +01:00
parent 6273bcdd3f
commit 62ab717772

View File

@@ -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}