From fe34b59590b3e0e487c9d866d731684a5623a8ba Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 5 Jun 2019 16:09:51 +0200
Subject: [PATCH] [gui] Default project in bold in project menu
---
src/plugins/gui/project_manager.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 61ef9946288..de946239370 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -197,7 +197,9 @@ let rec rename_project
and mk_project_entry window menu ?group p =
let pname = Project.get_unique_name p in
- let item = GMenu.menu_item ~label:pname ~packing:menu#append () in
+ let markup = if Project.is_current p then "<b>" ^ pname ^ "</b>" else pname in
+ let item = GMenu.menu_item ~packing:menu#append () in
+ let _label = GMisc.label ~markup ~packing:item#add () in
let submenu = GMenu.menu ~packing:item#set_submenu () in
let p_item = GMenu.radio_menu_item
?group
--
GitLab