Lerking/gdb-gui
1
0
Fork 0
mirror of https://github.com/tromey/gdb-gui.git synced 2026-01-04 15:40:06 +01:00
Code Issues Packages Projects Releases Wiki Activity

put window number and source basename in title bar

Browse Source
This commit is contained in:
Tom Tromey
2015-04-30 13:34:40 -06:00
parent 5b31fb182c
commit 35143e403f
2 changed files with 7 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
gui/source.py
View File

@@ -208,6 +208,7 @@ class SourceWindow(Toplevel):
lru_handler.add(self)
self.window.set_title('GDB Source @%d' % self.number)
self.window.show()
def deleted(self, widget, event):
@@ -232,6 +233,9 @@ class SourceWindow(Toplevel):
if buff is not None:
old_buffer = self.view.get_buffer()
self.view.set_buffer(buff)
# Might be good to let the user pick the format...
self.window.set_title('%s - GDB Source @%d'
% (os.path.basename(srcfile), self.number))
buffer_manager.release_buffer(old_buffer)
GObject.idle_add(self._do_scroll, buff, srcline - 1)
# self.view.scroll_to_iter(buff.get_iter_at_line(srcline), 0.0)