diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml index 62bf7fe30662135ed3441e8eec2e407578c007d7..61ef99462884007aa062f3a6e6e996c8855f1d1c 100644 --- a/src/plugins/gui/project_manager.ml +++ b/src/plugins/gui/project_manager.ml @@ -274,9 +274,12 @@ let () = let filter p' = not (Project.equal p p') in recompute ~filter window menu in + let hook () = recompute window menu in Project.register_create_hook callback_prj; Project.register_after_set_current_hook ~user_only:true callback_prj; Project.register_before_remove_hook callback_rm_prj; + Project.register_after_load_hook hook; + Project.register_after_global_load_hook hook; recompute window menu) (*