Skip to content
Snippets Groups Projects
Commit 8f0fca99 authored by Maxime Jacquemin's avatar Maxime Jacquemin
Browse files

Merge branch 'fix/gui/project-names' into 'master'

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

See merge request frama-c/frama-c!3491
parents 7f4dbf5f d40b1bca
No related branches found
No related tags found
No related merge requests found
...@@ -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% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment