From 24575797b246ab49aa0f07c87b76e2dd7667b1be Mon Sep 17 00:00:00 2001
From: eidheim <eidheim@gmail.com>
Date: Sun, 3 Apr 2016 22:33:16 +0200
Subject: [PATCH] Made the terminal font size 95% of the source font size. See
 #179

---
 src/window.cc | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/window.cc b/src/window.cc
index 19239e8..644032b 100644
--- a/src/window.cc
+++ b/src/window.cc
@@ -146,8 +146,11 @@ void Window::configure() {
   style_context->add_provider_for_screen(screen, css_provider, GTK_STYLE_PROVIDER_PRIORITY_SETTINGS);
   Directories::get().update();
   Menu::get().set_keys();
-  if(Config::get().source.font.size()>0)
-    Terminal::get().override_font(Pango::FontDescription(Config::get().source.font));
+  if(Config::get().source.font.size()>0) {
+    Pango::FontDescription font_description(Config::get().source.font);
+    font_description.set_size(font_description.get_size()*0.95);
+    Terminal::get().override_font(font_description);
+  }
 }
 
 void Window::set_menu_actions() {