From d9ae07c637a0e273672cbab67ad7d701cfc5856e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 4 Jun 2019 19:39:27 +0200
Subject: [PATCH] [gui] update menu label
---
src/plugins/gui/project_manager.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 9ee9502a373..62bf7fe3066 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -203,7 +203,7 @@ and mk_project_entry window menu ?group p =
?group
~active:(Project.is_current p)
~packing:submenu#append
- ~label:"current"
+ ~label:"Set current"
()
in
let callback () = if p_item#active then Project.set_current p in
--
GitLab