aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f17beb604..01805ab1e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1996,7 +1996,9 @@ let main files =
end
in
- let do_or_activate f = do_if_not_computing (do_or_activate f) in
+ let do_or_activate f =
+ do_if_not_computing (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+ in
let add_to_menu_toolbar text ~tooltip ~key ~callback icon =
ignore (navigation_factory#add_item text ~key ~callback);