From f6b03d1a0a38f9a7decc4452997a2397405f5fdb Mon Sep 17 00:00:00 2001
From: Fabian Jakobs <fabian.jakobs@web.de>
Date: Wed, 20 Oct 2010 13:25:00 +0200
Subject: [PATCH] make default font size smaller

---
 src/ace/theme/tm.css | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ace/theme/tm.css b/src/ace/theme/tm.css
index 2f7cdd73..be5ef74f 100644
--- a/src/ace/theme/tm.css
+++ b/src/ace/theme/tm.css
@@ -1,7 +1,7 @@
 .ace-tm .ace_editor {
   border: 2px solid rgb(159, 159, 159);
   font-family: "Menlo", "Monaco", "Courier New", "Courier", monospace;
-  font-size: 12px;  
+  font-size: 11px;  
 }
 
 .ace-tm .ace_editor.ace_focus {
@@ -12,8 +12,8 @@
   width: 50px;
   background: #e8e8e8;
   color: #333;
-  font-family: Menlo, Monaco, "Courier New";
-  font-size: 12px;
+  font-family: "Menlo", "Monaco", "Courier New", monospace;
+  font-size: 11px;
   overflow : hidden;
 }