diff options
Diffstat (limited to 'ide/document.mli')
| -rw-r--r-- | ide/document.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/ide/document.mli b/ide/document.mli index 8196c0f21..0d803ff00 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -106,13 +106,10 @@ val print : (** Callbacks on documents *) -class ['a] signals : - 'a GUtil.signal -> - 'a GUtil.signal -> +class type ['a] signals = object - inherit GUtil.ml_signals - method popped : callback:('a -> unit) -> GtkSignal.id - method pushed : callback:('a -> unit) -> GtkSignal.id + method popped : callback:('a -> unit) -> unit + method pushed : callback:('a -> unit) -> unit end val connect : 'a document -> 'a signals |