aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Find.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 19:36:45 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:33:39 +0200
commit2826683746569b9d78aa01e319315ab554e1619b (patch)
treeda0933c7169635d9e35003af4d40b0408e7de96d /ide/wg_Find.ml
parent8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (diff)
Fix omitted labels in function calls
Diffstat (limited to 'ide/wg_Find.ml')
-rw-r--r--ide/wg_Find.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 3d847ddcc..f84b9063b 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -186,8 +186,8 @@ class finder name (view : GText.view) =
in
let find_cb = generic_cb self#hide self#find_forward in
let replace_cb = generic_cb self#hide self#replace in
- let _ = find_entry#event#connect#key_press find_cb in
- let _ = replace_entry#event#connect#key_press replace_cb in
+ let _ = find_entry#event#connect#key_press ~callback:find_cb in
+ let _ = replace_entry#event#connect#key_press ~callback:replace_cb in
(** TextView interaction *)
let view_cb ev =
@@ -197,7 +197,7 @@ class finder name (view : GText.view) =
else false
else false
in
- let _ = view#event#connect#key_press view_cb in
+ let _ = view#event#connect#key_press ~callback:view_cb in
()
end