mirror of
https://gitlab.gnome.org/GNOME/gitg
synced 2024-10-02 14:13:48 +00:00
Destroy popover when hiding options
This commit is contained in:
parent
89a3c8168e
commit
6115250d59
|
@ -133,6 +133,7 @@ public class DiffViewOptions : Gtk.Grid
|
|||
private void on_button_developer_tools_clicked()
|
||||
{
|
||||
view.get_inspector().show();
|
||||
hide();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -603,6 +603,10 @@ namespace Gitg
|
|||
opts.show();
|
||||
m.show();
|
||||
|
||||
opts.notify["visible"].connect(() => {
|
||||
m.destroy();
|
||||
});
|
||||
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue