From 05964774e2e14cccdbcbc62ed6ca8bc855136036 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 5 Jun 2019 15:51:01 +0200
Subject: [PATCH] [gui] recompute project menu after loading projects
incidentally, this avoids having the phantom duplication of current project
when duplicating a non-current project.
---
src/plugins/gui/project_manager.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 62bf7fe3066..61ef9946288 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)
(*
--
GitLab