From ab2a98426e2f1cb9fdd6b8b701e0e33af28c45b8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?G=C3=A9ry=20Debongnie?= <ged@odoo.com>
Date: Fri, 3 May 2019 14:33:34 +0200
Subject: [PATCH] [IMP] playground: slightly decrease font size

---
 extras/playground/app.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/extras/playground/app.js b/extras/playground/app.js
index 181d3bd5..bf72dff3 100644
--- a/extras/playground/app.js
+++ b/extras/playground/app.js
@@ -81,7 +81,7 @@ class TabbedEditor extends owl.Component {
     // remove this for xml/css (?)
     this.editor.session.setOption("useWorker", false);
     this.editor.setValue(this.props[this.state.currentTab], -1);
-    this.editor.setFontSize("13px");
+    this.editor.setFontSize("12px");
     this.editor.setTheme("ace/theme/monokai");
     this.editor.session.setMode(MODES[this.state.currentTab]);
     const tabSize = this.state.currentTab === "xml" ? 2 : 4;