From b4b86b0478598e5f713cf09cca3f945ed6894ea9 Mon Sep 17 00:00:00 2001 From: markjcrane Date: Fri, 4 Mar 2016 13:18:30 -0700 Subject: [PATCH] Fix indentation on the editor. --- app/edit/index.php | 12 +++++++++++- themes/enhanced/template.php | 2 +- themes/minimized/template.php | 2 +- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/app/edit/index.php b/app/edit/index.php index 80eb11745e..1cd12b326a 100644 --- a/app/edit/index.php +++ b/app/edit/index.php @@ -59,12 +59,22 @@ else { $setting_indenting = ($_SESSION["editor"]["indent_guides"]["boolean"] != '') ? $_SESSION["editor"]["indent_guides"]["boolean"] : 'false'; $setting_numbering = ($_SESSION["editor"]["line_numbers"]["boolean"] != '') ? $_SESSION["editor"]["line_numbers"]["boolean"] : 'true'; $setting_preview = ($_SESSION["editor"]["live_preview"]["boolean"] != '') ? $_SESSION["editor"]["live_preview"]["boolean"] : 'true'; + +//get and then set the favicon + if (isset($_SESSION['theme']['favicon']['text'])){ + $favicon = $_SESSION['theme']['favicon']['text']; + } + else { + $favicon = '/themes/enhanced/favicon.ico'; + } + ?> - <?php echo $title;?> + <?php echo $title; ?> +