diff --git a/opam/opam b/opam/opam index 59c2ae9d96fd32559d40d8682e91ef386647a684..042f85254d724a2a229eda862168c41d5be07ad7 100644 --- a/opam/opam +++ b/opam/opam @@ -19,6 +19,7 @@ authors: [ "Julien Crétin" "Pascal Cuoq" "Zaynah Dargaye" + "Basile Desloges" "Jean-Christophe Filliâtre" "Philippe Herrmann" "Maxime Jacquemin" diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml index 68983f58f9e9e87bfba191d367b1426cad105654..286541b637bb8816a7015ce0921cfb21313000bb 100644 --- a/src/plugins/gui/help_manager.ml +++ b/src/plugins/gui/help_manager.ml @@ -37,6 +37,7 @@ let show main_ui = "Julien Crétin"; "Pascal Cuoq"; "Zaynah Dargaye"; + "Basile Desloges"; "Jean-Christophe Filliâtre"; "Philippe Herrmann"; "Maxime Jacquemin";