aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/document.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/document.mli')
-rw-r--r--ide/document.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/document.mli b/ide/document.mli
index 0d803ff00..fb96cb6d7 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -108,8 +108,8 @@ val print :
class type ['a] signals =
object
- method popped : callback:('a -> unit) -> unit
- method pushed : callback:('a -> unit) -> unit
+ method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+ method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
end
val connect : 'a document -> 'a signals