From 2065b4138a33bf16d16162076bb18df255621be2 Mon Sep 17 00:00:00 2001
From: Tom Tromey <tom@tromey.com>
Date: Tue, 5 May 2015 10:25:45 -0600
Subject: [PATCH] update titles when changed

---
 gui/params.py   |  2 +-
 gui/toplevel.py | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/gui/params.py b/gui/params.py
index 97bc6b2..e324133 100644
--- a/gui/params.py
+++ b/gui/params.py
@@ -167,7 +167,7 @@ class _Title(_StoredParameter):
     @in_gdb_thread
     def get_set_string(self):
         super(_Title, self).get_set_string()
-        # gui.toplevel.state.set_font(self.value)
+        gui.toplevel.state.update_titles()
         return ""
 
 _SetBase()
diff --git a/gui/toplevel.py b/gui/toplevel.py
index fb499e0..bde6f03 100644
--- a/gui/toplevel.py
+++ b/gui/toplevel.py
@@ -73,6 +73,16 @@ class _ToplevelState(object):
     def set_font(self, font_name):
         gui.startup.send_to_gtk(lambda: self._do_set_font(font_name))
 
+    @in_gtk_thread
+    def _do_update_titles(self):
+        with self.toplevel_lock:
+            for num in self.toplevels:
+                self.toplevels[num].update_title()
+
+    @in_gdb_thread
+    def update_titles(self):
+        gui.startup.send_to_gtk(lambda: self._do_update_titles))
+
     @in_gtk_thread
     def windows(self):
         return self.toplevels.values()