summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/undo_lablgtk_ge212.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index 916a06e9..4488b5e9 100644
--- a/ide/undo_lablgtk_ge212.mli
+++ b/ide/undo_lablgtk_ge212.mli
@@ -10,9 +10,10 @@
(* An undoable view class *)
-class undoable_view : [> Gtk.text_view] Gtk.obj ->
+class undoable_view : ([> Gtk.text_view] as 'a) Gtk.obj ->
object
inherit GText.view
+ val obj : 'a Gtk.obj
method undo : bool
method redo : bool
method clear_undo : unit