diff options
| author | Hugo Herbelin | 2018-11-03 15:55:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-10 12:03:18 +0200 |
| commit | 0cb8482b51f25b2f705f4da28f08424f48fa9c93 (patch) | |
| tree | ef6e4c65450696cb8eb27a762ca99fba882a0848 /ide | |
| parent | 968f9b59f390182c3123217dd5b13f80a2ee08c2 (diff) | |
Hack to have the "ready" status bar message not hiding flash notices.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/coqide_main.ml | 1 |
2 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 9cdfd0dc21..fb08195308 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1247,7 +1247,6 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml index 6f4c0ece31..1e04d269f6 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.ml @@ -52,6 +52,7 @@ let load_prefs () = Preferences.load_pref ~warn:(fun ~delay -> Ideutils.flash_info ~delay) let () = + Ideutils.push_info ("Ready"^ if Preferences.microPG#get then ", [μPG]" else ""); load_prefs (); let argl = List.tl (Array.to_list Sys.argv) in let argl = Coqide.read_coqide_args argl in |