reducing font size of terminals; push buttons to top

[pygdb.git] / DbgTerminal.py

diff --git a/DbgTerminal.py b/DbgTerminal.py
index 7c494458000fb40005486ea9f8b85f64849ec4ee..605c2b79612823a92f4955f935517737b142f856 100644 (file)
--- a/DbgTerminal.py
+++ b/DbgTerminal.py
@@ -5,6 +5,7 @@ __author__ = "shuber"
 
 
 import gtk
+import pango
 import pty
 import string
 import time
@@ -38,6 +39,10 @@ class DbgTerminal (vte.Terminal):
                self.connect("cursor-moved", self.contents_changed)
                self.connect("child-exited", lambda *w: gtk.main_quit())
 
+               fontdesc = pango.FontDescription("monospace 9")
+               self.set_font(fontdesc)
+
+
 
        def contents_changed(self, term):
                c,r = term.get_cursor_position()