aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ide/coqide.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 39dcd0ffa0..9bed066669 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2211,6 +2211,9 @@ let main files =
find_w#misc#hide();
v#coerce#misc#grab_focus()
in
+ to_do_on_page_switch :=
+ (fun i -> if find_w#misc#visible then close_find())::
+ !to_do_on_page_switch;
let find_again_forward () =
search_backward := false;
let (v,b,start,_) = last_find () in