[gitg] Destroy popover when hiding options

[Jesse van den Kieboom <jessevdk src gnome org>]

commit 6115250d59106ea5b59f03414dc5538f853ed0e8
Author: Jesse van den Kieboom <jessevdk gnome org>
Date:   Thu Jul 10 19:10:38 2014 +0200

    Destroy popover when hiding options

 libgitg/gitg-diff-view-options.vala |    1 +
 libgitg/gitg-diff-view.vala         |    4 ++++
 2 files changed, 5 insertions(+), 0 deletions(-)
---
diff --git a/libgitg/gitg-diff-view-options.vala b/libgitg/gitg-diff-view-options.vala
index 9b6b821..e353c94 100644
--- a/libgitg/gitg-diff-view-options.vala
+++ b/libgitg/gitg-diff-view-options.vala
@@ -133,6 +133,7 @@ public class DiffViewOptions : Gtk.Grid
        private void on_button_developer_tools_clicked()
        {
                view.get_inspector().show();
+               hide();
        }
 }
 
diff --git a/libgitg/gitg-diff-view.vala b/libgitg/gitg-diff-view.vala
index 9ea2ec0..19b6286 100644
--- a/libgitg/gitg-diff-view.vala
+++ b/libgitg/gitg-diff-view.vala
@@ -603,6 +603,10 @@ namespace Gitg
                        opts.show();
                        m.show();
 
+                       opts.notify["visible"].connect(() => {
+                               m.destroy();
+                       });
+
                        return true;
                }
        }