From 381fa8fe28fd5a93854f0eed108d854256f81258 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Wed, 27 Nov 2019 10:43:39 +0100 Subject: [PATCH] [Gui] fix assertion (fixes #769) --- 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 2e60e840184..d2f20659e5a 100644 --- a/src/plugins/gui/project_manager.ml +++ b/src/plugins/gui/project_manager.ml @@ -251,7 +251,7 @@ and mk_project_entry window menu ?group p = and make_project_entries ?filter window menu = match projects_list ?filter () with - | [] -> assert false + | [] -> assert (filter <> None) | (pa, _name) :: tl -> let mk = mk_project_entry window menu in let pa_item = mk pa in -- GitLab