From 1b5d54b58f4ecea66ef9bf439d23b115d2c77050 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 1 Jan 2016 23:29:11 +0100
Subject: Remove unplugged button from the interface.

---
 ide/preferences.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'ide/preferences.ml')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index a605014f2..3d11e94fe 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -700,10 +700,6 @@ let configure ?(apply=(fun () -> ())) () =
       ~border_width:2
       ~packing:scroll#add_with_viewport ()
     in
-    let reset_button = GButton.button
-      ~label:"Reset"
-      ~packing:box#pack ()
-    in
     let i = ref 0 in
     let cb = ref [] in
     let iter text tag =
-- 
cgit v1.2.3