diff options
Diffstat (limited to 'ide/wg_Find.mli')
| -rw-r--r-- | ide/wg_Find.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli index 5337dae7c..a8e734887 100644 --- a/ide/wg_Find.mli +++ b/ide/wg_Find.mli @@ -6,13 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type mode = [ `FIND | `REPLACE ] - -class finder : GText.view -> +class finder : string -> GText.view -> object method coerce : GObj.widget method hide : unit -> unit - method show : mode -> unit + method show : unit -> unit method replace : unit -> unit method replace_all : unit -> unit method find_backward : unit -> unit |