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 = ';