Merge pull request #710 from Eyenseo/master

Fix different font sizes in editor and code
rust-lang · Jul 24, 2018 · b88abb1 · b88abb1
2 parents 7c8dd50 + b452d5e
commit b88abb1
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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 {
-Original file line number
+Diff line change
@@ Expand Up / @@ -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 {
@@ Expand Down @@