From b452d5e0c7c9af211733f441880112e63ea74bd2 Mon Sep 17 00:00:00 2001
From: eyenseo <eyenseo@gmail.com>
Date: Tue, 19 Jun 2018 22:28:23 +0200
Subject: [PATCH] Fix different font sizes in editor and code

Fixes #705
---
 src/theme/playpen_editor/editor.js | 3 ++-
 src/theme/stylus/general.styl      | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/theme/playpen_editor/editor.js b/src/theme/playpen_editor/editor.js
index 4e3bdcaf..7c32f851 100644
--- a/src/theme/playpen_editor/editor.js
+++ b/src/theme/playpen_editor/editor.js
@@ -12,7 +12,8 @@ window.editors = [];
             showPrintMargin: false,
             showLineNumbers: false,
             showGutter: false,
-            maxLines: Infinity
+            maxLines: Infinity,
+            fontSize: "0.875em" // please adjust the font size of the code in general.styl
         });
 
         editor.$blockScrolling = Infinity;
diff --git a/src/theme/stylus/general.styl b/src/theme/stylus/general.styl
index ead07bf3..0420a862 100644
--- a/src/theme/stylus/general.styl
+++ b/src/theme/stylus/general.styl
@@ -11,7 +11,7 @@ body {
 
 code {
     font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace;
-    font-size: 0.875em;
+    font-size: 0.875em; // please adjust the ace font size accordingly in editor.js
 }
 
 .left {