Skip to content
Snippets Groups Projects
Commit d40b1bca authored by David Bühler's avatar David Bühler Committed by Maxime Jacquemin
Browse files

[gui] In the project menu, fixes project names containing the character '&'.

parent 82124f2b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/gui/project_manager.ml
+ 1
− 1
View file @ d40b1bca
...@@ -140,7 +140,7 @@ let load_project (host_window: Design.main_window_extension_points) = ...@@ -140,7 +140,7 @@ let load_project (host_window: Design.main_window_extension_points) =
dialog#destroy () dialog#destroy ()
let mk_project_markup p = let mk_project_markup p =
let name = Project.get_unique_name p in let name = Extlib.html_escape (Project.get_unique_name p) in
if Project.is_current p then "<b>" ^ name ^ "</b>" else name if Project.is_current p then "<b>" ^ name ^ "</b>" else name
let reset ?filter (menu: GMenu.menu) = let reset ?filter (menu: GMenu.menu) =
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment