diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml index 9ee9502a37378be458dff0e86ec45c49eabf55a3..62bf7fe30662135ed3441e8eec2e407578c007d7 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