Fix different font sizes in editor and code

Fixes #705
2018-06-19 22:28:23 +02:00 · 2018-06-19 22:28:23 +02:00 · b452d5e0c7
parent 2a55ff62f3
commit b452d5e0c7
2 changed files with 3 additions and 2 deletions
--- 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;
--- 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 {