From 74c29764359272b29af081b30762549777ae8825 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 2 Jan 2016 17:05:03 +0100
Subject: Remove some useless type declarations.

---
 ide/wg_Find.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'ide/wg_Find.ml')

diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index a0949ca0c..dc7071c27 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type mode = [ `FIND | `REPLACE ]
-
 let b2c = Ideutils.byte_offset_to_char_offset
 
 class finder name (view : GText.view) =
-- 
cgit v1.2.3